From 5fe77c3cb1b3485f8128e0f184b6027be042740a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 24 Jan 2011 14:28:17 +0000 Subject: [PATCH] Fix. Ooops. I'd commented out the fix of r1082 / r1083. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1089 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 73956d6..47a0fa9 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -118,8 +118,8 @@ namespace BEEV { // 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); + if (initialSize != simp->Return_SolverMap()->size()) + simplified_solved_InputToSAT = simp->applySubstitutionMapUntilArrays(simplified_solved_InputToSAT); simplified_solved_InputToSAT = -- 2.47.3