From 019cf84d1cc8dbef439d9be6bb01797d88f3e930 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 23 Jan 2011 00:57:04 +0000 Subject: [PATCH] Bugfix. An assertion error would be produced because a term was not simplified. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1082 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index e5bdf7e..73956d6 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -103,13 +103,24 @@ namespace BEEV { if(bm->UserFlags.optimize_flag) { + int initialSize = simp->Return_SolverMap()->size(); + simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); - //printf("##################################################\n"); bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); + // Imagine: + // The simplifier simplifies (0 + T) to T + // Then bvsolve introduces (0 + T) + // Then CreateSubstitutionMap decides T maps to a constant, but leaving another (0+T). + // When we go to simplify (0 + T) will still be in the simplify cache, so will be mapped to T. + // But it shouldn't be T, it should be a constant. + // Applying the substitution map fixes this unusual case... expensively... + // if (initialSize != simp->Return_SolverMap()->size()) + // simplified_solved_InputToSAT = simp->applySubstitutionMapUntilArrays(simplified_solved_InputToSAT); + simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, -- 2.47.3