Fixing two bugs:

1) arithmetic should check for subterms when solving equations, for instance x = if b then x + 1 else x -1 is not a valid substitution
2) a memory problem in minisat - explanations are constructed during conflict analysis, so the clause database might resize and relocate, which invalidates any references to clauses

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index c2d53bef82864ca17026ec4406fb21fe46bf4a3b..1ec9b0962412a44fc1169d4d4ffff3035519f6b2 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -565,14 +565,19 @@ int Solver::litRedundant(Lit p, uint32_t abstract_levels)
     int top = analyze_toclear.size();
     int max_level = 0;
     while (analyze_stack.size() > 0){
-        assert(reason(var(analyze_stack.last())) != CRef_Undef);
-        Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop();
+        CRef c_reason = reason(var(analyze_stack.last()));
+        assert(c_reason != CRef_Undef);
+        Clause& c = ca[c_reason];
+        int c_size = c.size();
+        analyze_stack.pop();
         if (c.level() > max_level) {
             max_level = c.level();
         }
 
-        for (int i = 1; i < c.size(); i++){
-            Lit p  = c[i];
+        // Since calling reason might relocate to resize, c is not necesserily the right reference, we must
+        // use the allocator each time
+        for (int i = 1; i < c_size; i++){
+            Lit p  = ca[c_reason][i];
             if (!seen[var(p)] && level(var(p)) > 0){
                 if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){
                     seen[var(p)] = 1;

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 34cb4d666caa9efaaf9957ec9c84d0734fffe65d..93c02942ddf39c12de5ad03a87966df43a9a2e05 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -184,9 +184,12 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio
       }
       // x = (p - ax - c) * -1/a
       eliminateVar = NodeManager::currentNM()->mkNode(kind::MULT, eliminateVar, mkRationalNode(- minConstant.inverse()));
-      // Add the substitution
-      outSubstitutions.addSubstitution(minVar, Rewriter::rewrite(eliminateVar));
-      return SOLVE_STATUS_SOLVED;
+      // Add the substitution if not recursive
+      Node rewritten = Rewriter::rewrite(eliminateVar);
+      if (!rewritten.hasSubterm(minVar)) {
+        outSubstitutions.addSubstitution(minVar, Rewriter::rewrite(eliminateVar));
+        return SOLVE_STATUS_SOLVED;
+      }
     }
   }