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 

1 files changed, 6 insertions, 3 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 34cb4d666..93c02942d 100644
--- 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;
+      }
     }
   }