From 684215b52755182678889f0df5c69e821da3e0c6 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Wed, 6 Jul 2011 23:42:04 +0000 Subject: 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 --- src/theory/arith/theory_arith.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'src/theory/arith/theory_arith.cpp') 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; + } } } -- cgit v1.2.3