From 15ccd3a0e32022cde86d7bfa5c2d51b655d14dcf Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 28 Jan 2012 13:57:37 +0000 Subject: [PATCH] Fix an assertion error. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1535 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/PropagateEqualities.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp index d3225f0..90fd4b1 100644 --- a/src/simplifier/PropagateEqualities.cpp +++ b/src/simplifier/PropagateEqualities.cpp @@ -21,7 +21,11 @@ namespace BEEV Kind k = lhs.GetKind(); if (k == SYMBOL) - return simp->UpdateSubstitutionMap(lhs, rhs); // checks whether it's been solved for or loops. + { + if (lhs == rhs) + return true; + return simp->UpdateSubstitutionMap(lhs, rhs); // checks whether it's been solved for or loops. + } if (k == NOT) return searchXOR(lhs[0], nf->CreateNode(NOT, rhs)); @@ -61,7 +65,12 @@ namespace BEEV const int width = lhs.GetValueWidth(); if (lhs.GetKind() == SYMBOL) - return simp->UpdateSubstitutionMap(lhs, rhs); // checks whether it's been solved for, or if the RHS contains the LHS. + { + if (lhs == rhs) + return true; + + return simp->UpdateSubstitutionMap(lhs, rhs); // checks whether it's been solved for, or if the RHS contains the LHS. + } if (lhs.GetKind() == BVUMINUS) return searchTerm(lhs[0], nf->CreateTerm(BVUMINUS, width, rhs)); -- 2.47.3