Make sure free symbols are declared in SMT2_conv after quantifier rewriting

Author: qinheping

regression/contracts-dfcc/quantifiers-loop-05/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stddef.h>
+
+#define N 16
+
+void main()
+{
+  int a[N];
+  a[10] = 0;
+  bool flag = true;
+  for(size_t j = 0; j < N; ++j)
+    // clang-format off
+  __CPROVER_assigns(j, __CPROVER_object_whole(a))
+  __CPROVER_loop_invariant(j <= N)
+  __CPROVER_loop_invariant((j != 0) ==> __CPROVER_forall {
+        int k;
+        (0 <= k && k < N) ==> (a[k] == 1)
+  })
+    // clang-format on
+    {
+      for(size_t i = 0; i < N; ++i)
+        // clang-format off
+      __CPROVER_assigns(i, __CPROVER_object_whole(a))
+      __CPROVER_loop_invariant(0 <= i && i <= N)
+      __CPROVER_loop_invariant(__CPROVER_forall { int k; k < i ==> a[k] == 1 })
+
+        // clang-format on
+        {
+          a[i] = 1;
+        }
+    }
+  assert(a[10] == 1);
+}

regression/contracts-dfcc/quantifiers-loop-fail/test.desc renamed to regression/contracts-dfcc/quantifiers-loop-05/test.desc

@@ -1,11 +1,9 @@
 CORE dfcc-only
 main.c
 --dfcc main --apply-loop-contracts _ --smt2
-^EXIT=6$
+^EXIT=0$
 ^SIGNAL=0$
-^SMT2 solver returned error message:$
-^.*\"line \d+ column \d+: unknown constant .*$
-^VERIFICATION ERROR$
+^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
 --

regression/contracts-dfcc/quantifiers-loop-fail/main.c

@@ -4908,17 +4908,30 @@ void smt2_convt::find_symbols(const exprt &expr)
 
   if(expr.id() == ID_exists || expr.id() == ID_forall)
   {
+    std::unordered_map<irep_idt, std::optional<identifiert>> hidden_syms;
+
     // do not declare the quantified symbol, but record
     // as 'bound symbol'
     const auto &q_expr = to_quantifier_expr(expr);
     for(const auto &symbol : q_expr.variables())
     {
       const auto identifier = symbol.get_identifier();
-      identifiert &id = identifier_map[identifier];
-      id.type = symbol.type();
-      id.is_bound = true;
+      auto id_entry = identifier_map.insert({identifier, identifiert{}});
+      hidden_syms.insert(
+        {identifier,
+         id_entry.second ? std::nullopt
+                         : std::optional{id_entry.first->second}});
+      id_entry.first->second.is_bound = true;
     }
     find_symbols(q_expr.where());
+    for(const auto &[id, hidden_val] : hidden_syms)
+    {
+      auto previous_entry = identifier_map.find(id);
+      if(!hidden_val.has_value())
+        identifier_map.erase(previous_entry);
+      else
+        previous_entry->second = std::move(*hidden_val);
+    }
     return;
   }
 
@@ -4943,7 +4956,7 @@ void smt2_convt::find_symbols(const exprt &expr)
 
     identifiert &id=identifier_map[identifier];
 
-    if(id.type.is_nil())
+    if(!id.is_bound && id.type.is_nil())
     {
       id.type=expr.type();