Merge pull request #3640 from diffblue/smt2-bound-symbols

smt2: fix exists/forall

Author: tautschnig

scripts/delete_failing_smt2_solver_tests

@@ -53,10 +53,7 @@ rm Pointer_byte_extract9/test.desc
 rm Promotion3/test.desc
 rm Quantifiers-assertion/test.desc
 rm Quantifiers-assignment/test.desc
-rm Quantifiers-if/test.desc
-rm Quantifiers-initialisation2/test.desc
 rm Quantifiers-invalid-var-range/test.desc
-rm Quantifiers-not/test.desc
 rm Quantifiers-type/test.desc
 rm Struct_Bytewise2/test.desc
 rm Union_Initialization1/test.desc

src/solvers/smt2/smt2_conv.cpp

@@ -4175,6 +4175,19 @@ void smt2_convt::find_symbols(const exprt &expr)
   // recursive call on type
   find_symbols(expr.type());
 
+  if(expr.id() == ID_exists || expr.id() == ID_forall)
+  {
+    // do not declare the quantified symbol, but record
+    // as 'bound symbol'
+    const auto &q_expr = to_quantifier_expr(expr);
+    const auto identifier = q_expr.symbol().get_identifier();
+    identifiert &id = identifier_map[identifier];
+    id.type = q_expr.symbol().type();
+    id.is_bound = true;
+    find_symbols(q_expr.where());
+    return;
+  }
+
   // recursive call on operands
   forall_operands(it, expr)
     find_symbols(*it);

src/solvers/smt2/smt2_conv.h

@@ -284,10 +284,11 @@ class smt2_convt:public prop_convt
   // keeps track of all non-Boolean symbols and their value
   struct identifiert
   {
+    bool is_bound;
     typet type;
     exprt value;
 
-    identifiert()
+    identifiert() : is_bound(false)
     {
       type.make_nil();
       value.make_nil();