Small fix

lib/Core/Executor.cpp

@@ -1460,9 +1460,9 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
 
   if (!concretization.isEmpty()) {
     // Update memory objects if arrays have affected them.
+    updateStateWithSymcretes(state, concretization);
     Assignment delta =
         state.constraints.cs().concretization().diffWith(concretization);
-    updateStateWithSymcretes(state, delta);
     state.addConstraint(condition, delta);
   } else {
     state.addConstraint(condition, {});
@@ -6490,7 +6490,7 @@ void Executor::updateStateWithSymcretes(ExecutionState &state,
    * assign. We want to update only objects, whose size were changed. */
 
   std::vector<ref<SizeSymcrete>> updatedSizeSymcretes;
-  const Assignment &diffAssignment =
+  Assignment diffAssignment =
       state.constraints.cs().concretization().diffWith(assignment);
 
   for (const ref<Symcrete> &symcrete : state.constraints.cs().symcretes()) {

lib/Expr/Constraints.cpp

@@ -209,7 +209,7 @@ ConstraintSet::ConstraintSet() {}
 void ConstraintSet::addConstraint(ref<Expr> e, const Assignment &delta) {
   _constraints.insert(e);
   // Update bindings
-  for (auto i : delta.bindings) {
+  for (auto &i : delta.bindings) {
     _concretization.bindings.replace({i.first, i.second});
   }
   _independentElements.updateConcretization(delta);

lib/Expr/IndependentSet.cpp

@@ -23,7 +23,7 @@ IndependentConstraintSet::updateConcretization(
   if (delta.bindings.size() == 0) {
     return ics;
   }
-  for (auto i : delta.bindings) {
+  for (auto &i : delta.bindings) {
     ics->concretization.bindings.replace({i.first, i.second});
   }
   InnerSetUnion DSU;
@@ -45,6 +45,15 @@ IndependentConstraintSet::updateConcretization(
     }
     DSU.addValue(new ExprEitherSymcrete::left(e));
   }
+  auto concretizationConstraints =
+      ics->concretization.createConstraintsFromAssignment();
+  for (ref<Expr> e : concretizationConstraints) {
+    if (auto ce = dyn_cast<ConstantExpr>(e)) {
+      assert(ce->isTrue() && "Attempt to add invalid constraint");
+      continue;
+    }
+    DSU.addValue(new ExprEitherSymcrete::left(e));
+  }
   ics->concretizedSets = DSU;
   return ics;
 }
@@ -56,7 +65,7 @@ IndependentConstraintSet::removeConcretization(
   if (delta.bindings.size() == 0) {
     return ics;
   }
-  for (auto i : delta.bindings) {
+  for (auto &i : delta.bindings) {
     ics->concretization.bindings.remove(i.first);
   }
   InnerSetUnion DSU;
@@ -78,6 +87,15 @@ IndependentConstraintSet::removeConcretization(
     }
     DSU.addValue(new ExprEitherSymcrete::left(e));
   }
+  auto concretizationConstraints =
+      ics->concretization.createConstraintsFromAssignment();
+  for (ref<Expr> e : concretizationConstraints) {
+    if (auto ce = dyn_cast<ConstantExpr>(e)) {
+      assert(ce->isTrue() && "Attempt to add invalid constraint");
+      continue;
+    }
+    DSU.addValue(new ExprEitherSymcrete::left(e));
+  }
 
   ics->concretizedSets = DSU;
   return ics;
@@ -343,6 +361,15 @@ IndependentConstraintSet::merge(ref<const IndependentConstraintSet> A,
       }
       DSU.addValue(new ExprEitherSymcrete::left(e));
     }
+    auto concretizationConstraints =
+        a->concretization.createConstraintsFromAssignment();
+    for (ref<Expr> e : concretizationConstraints) {
+      if (auto ce = dyn_cast<ConstantExpr>(e)) {
+        assert(ce->isTrue() && "Attempt to add invalid constraint");
+        continue;
+      }
+      DSU.addValue(new ExprEitherSymcrete::left(e));
+    }
 
     a->concretizedSets = DSU;
   }

scripts/kleef

@@ -92,6 +92,7 @@ def klee_options(
             "--track-coverage=all", # Only branches and only instructions are wrong in real life. E.g., ternary operators are sometimes counted as different branches, while we stick to look at them as a single instruction from a single branch
             "--use-iterative-deepening-search=max-cycles",
             f"--max-solver-time={MAX_SOLVER_TIME}s",
+            "--max-cycles-before-stuck=15",
             # "--tc-type=cov",
             "--only-output-states-covering-new",  # Don't generate all test cases
             "--dump-states-on-halt=true",  # Check in case we missed some oncovered instructions

test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c

@@ -9,7 +9,7 @@
 
 // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK-COV %s
 
-// Branch coverage 100%, the number of branches is 1:
+// Branch coverage 100%, the number of branches is 2:
 // CHECK-COV: Lines executed:100.00% of 11
 // CHECK-COV-NEXT: Branches executed:100.00% of 2
 // CHECK-COV-NEXT: Taken at least once:100.00% of 2

test/Industry/CoverageBranches/CostasArray-17.c

@@ -19,7 +19,7 @@
 
 // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s
 
-// Branch coverage 100%, the number of branches is 1:
+// Branch coverage 100%, the number of branches is 2:
 // CHECK: Lines executed:{{(0\.7[0-9])}}% of 1545
 // CHECK-NEXT: Branches executed:100.00% of 2
 // CHECK-NEXT: Taken at least once:100.00% of 2

test/Industry/CoverageBranches/egcd3-ll_valuebound10.c

@@ -9,7 +9,6 @@
 
 // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s
 
-// Branch coverage 100%, the number of branches is 1:
 // CHECK: Lines executed:87.93% of 58
 // CHECK-NEXT: Branches executed:100.00% of 18
 // CHECK-NEXT: Taken at least once:83.33% of 18

test/Industry/CoverageBranches/matrix-2-2.c

@@ -0,0 +1,68 @@
+// RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=all --max-cycles=2 --optimize=true --emit-all-errors --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=true --use-sym-size-alloc=true --symbolic-allocation-threshold=8192 %t1.bc 2>&1
+
+// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov
+// RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage
+// RUN: %replay %t.klee-out %t_runner
+// RUN: gcov -b %t_runner-%basename_t > %t.cov.log
+
+// RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK-COV %s
+
+// Branch coverage is greater 80%:
+// CHECK-COV: Lines executed:9{{([0-9]\.[0-9][0-9])}}% of 24
+// CHECK-COV-NEXT: Branches executed:100.00% of 16
+// CHECK-COV-NEXT: Taken at least once:{{([8-9][0-9]\.[0-9][0-9])}}% of 16
+
+#include "klee-test-comp.c"
+
+extern void exit(int);
+extern void abort(void);
+#ifdef GCOV
+extern void __gcov_dump(void);
+#endif
+
+void dump() {
+#ifdef GCOV
+  __gcov_dump();
+  exit(0);
+#endif
+}
+
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { dump(); __assert_fail("0", "matrix-2-2.c", 3, "reach_error"); }
+
+void __VERIFIER_assert(int cond) {
+  if (!(cond)) {
+    ERROR: {reach_error();abort();}
+  }
+  return;
+}
+extern unsigned int __VERIFIER_nondet_uint();
+extern int __VERIFIER_nondet_int();
+
+int main()
+{
+  unsigned int N_LIN=__VERIFIER_nondet_uint();
+  unsigned int N_COL=__VERIFIER_nondet_uint();
+  if (N_LIN >= 4000000000 / sizeof(int) || N_COL >= 4000000000 / sizeof(int)) {
+    return 0;
+  }
+  unsigned int j,k;
+  int matriz[N_COL][N_LIN], maior;
+
+  maior = __VERIFIER_nondet_int();
+  for(j=0;j<N_COL;j++)
+    for(k=0;k<N_LIN;k++)
+    {       
+       matriz[j][k] = __VERIFIER_nondet_int();
+
+       if(matriz[j][k]>maior)
+          maior = matriz[j][k];                          
+    }                       
+
+  for(j=0;j<N_COL;j++)
+    for(k=0;k<N_LIN;k++)
+      __VERIFIER_assert(matriz[j][k]<maior);    
+}
+

test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c

@@ -10,7 +10,6 @@
 
 // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s
 
-// Branch coverage 89.29%
 // CHECK: Lines executed:{{(9[0-9]\.[0-9][0-9])}}% of 4114
 // CHECK-NEXT: Branches executed:{{(9[0-9]\.[0-9][0-9])}}% of 13404
 // CHECK-NEXT: Taken at least once:{{(8[0-9]\.[0-9][0-9])}}% of 13404