Disallow enumerate equal expr between sub-exprs with different types.

Author: qinheping

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.cpp

@@ -48,9 +48,14 @@ std::vector<exprt> construct_terminals(std::set<symbol_exprt> symbols)
       // For a variable v with primitive type, we add
       // v, __CPROVER_loop_entry(v)
       // into the result.
-      result.push_back(e);
+      result.push_back(typecast_exprt(e, size_type()));
       result.push_back(unary_exprt(ID_loop_entry, e, size_type()));
     }
+    if((e.type().id() == ID_signedbv))
+    {
+      result.push_back(e);
+      result.push_back(unary_exprt(ID_loop_entry, e, e.type()));
+    }
     if((e.type().id() == ID_pointer))
     {
       // For a variable v with pointer type, we add
@@ -62,7 +67,8 @@ std::vector<exprt> construct_terminals(std::set<symbol_exprt> symbols)
         unary_exprt(ID_loop_entry, e, e.type()), size_type()));
     }
   }
-  result.push_back(from_integer(1, size_type()));
+  result.push_back(from_integer(1, unsigned_int_type()));
+  result.push_back(from_integer(1, unsigned_long_int_type()));
   return result;
 }
 

src/goto-instrument/synthesizer/expr_enumerator.cpp

@@ -316,7 +316,12 @@ exprt binary_functional_enumeratort::instantiate(const expr_listt &exprs) const
     exprs.size() == 2,
     "number of arguments should be 2: " + integer2string(exprs.size()));
   if(op_id == ID_equal)
+  {
+    if(exprs.front().type() != exprs.back().type())
+      return true_exprt();
+
     return equal_exprt(exprs.front(), exprs.back());
+  }
   if(op_id == ID_le)
     return less_than_or_equal_exprt(exprs.front(), exprs.back());
   if(op_id == ID_lt)

src/goto-programs/CMakeLists.txt

@@ -3,4 +3,4 @@ add_library(goto-programs ${sources})
 
 generic_includes(goto-programs)
 
-target_link_libraries(goto-programs util assembler langapi analyses linking ansi-c)
+target_link_libraries(goto-programs util assembler langapi analyses linking ansi-c json)