formalsec / smtml / 585

42%

push

github

Fix model generation for expressions with different return types

Model generation for expressions like `str.len "a"` would return `Str
"1"` instead of `Int 1` because `value_of_term` would pass the type of
the theory of the expressions instead of the return type of the
expression. This commit addresses it by introducing a new
`Expr.return_type` function which correctly returns the return type of
an expression instead of the theory of which the expression is encoded
in.

27 of 49 new or added lines in 2 files covered. (55.1%)

2516 of 6154 relevant lines covered (40.88%)

36.15 hits per line