Add equal expressions in quantified symbol detection for loop contracts

Author: qinheping

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

@@ -1,18 +1,20 @@
 #include <assert.h>
+#include <stdbool.h>
 
 #define N 16
 
 void main()
 {
   int a[N];
   a[10] = 0;
+  bool flag = true;
 
   for(int i = 0; i < N; ++i)
     // clang-format off
     __CPROVER_assigns(i, __CPROVER_object_whole(a))
     __CPROVER_loop_invariant(
       (0 <= i) && (i <= N) &&
-      __CPROVER_forall {
+      flag == __CPROVER_forall {
         int k;
         // constant bounds for explicit unrolling with SAT backend
         (0 <= k && k <= N) ==> (

regression/contracts/quantifiers-loop-01/main.c

@@ -1,18 +1,20 @@
 #include <assert.h>
+#include <stdbool.h>
 
 #define N 16
 
 void main()
 {
   int a[N];
   a[10] = 0;
+  bool flag = true;
 
   for(int i = 0; i < N; ++i)
     // clang-format off
     __CPROVER_assigns(i, __CPROVER_object_whole(a))
     __CPROVER_loop_invariant(
       (0 <= i) && (i <= N) &&
-      __CPROVER_forall {
+      flag == __CPROVER_forall {
         int k;
         // constant bounds for explicit unrolling with SAT backend
         (0 <= k && k <= N) ==> (

src/goto-instrument/contracts/utils.cpp

@@ -376,7 +376,9 @@ void add_quantified_variable(
     auto &unary_expression = to_unary_expr(expression);
     add_quantified_variable(symbol_table, unary_expression.op(), mode);
   }
-  if(expression.id() == ID_notequal || expression.id() == ID_implies)
+  if(
+    expression.id() == ID_notequal || expression.id() == ID_equal ||
+    expression.id() == ID_implies)
   {
     // For binary connectives, recursively check for
     // nested quantified formulae in the left and right terms

src/goto-symex/renaming_level.cpp

@@ -17,6 +17,7 @@ Author: Romain Brenguier, [email protected]
 #include <util/symbol.h>
 
 #include "goto_symex_state.h"
+#include <iostream>
 
 renamedt<ssa_exprt, L0>
 symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)