Merge pull request #983 from diffblue/smv-typecheck-expr

SMV: separate type checking and type conversion

Author: kroening

regression/smv/boolean/boolean_expected5.desc

@@ -1,7 +1,7 @@
 CORE
 boolean_expected5.smv
 
-^file boolean_expected5\.smv line 5: Expected expression of type `boolean', but got expression `a', which is of type `\{  \}'$
+^file boolean_expected5\.smv line 5: Expected expression of type `boolean', but got expression `a', which is of type `\{ a \}'$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/range-type/range_type5.desc

@@ -1,8 +1,7 @@
 CORE broken-smt-backend
 range_type5.smv
 --bound 3
-^file .* line 14: Expected expression of type `5..10', but got expression `x', which is of type `0..6'$
-^EXIT=2$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/smv/range-type/range_type8.desc

@@ -1,9 +1,8 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 range_type8.smv
 --bound 5
 ^\[spec1\] G x != 1: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 --
-We do not have type checking for unary minus.