From 4f901a649205c42f5e1f5dfab2ed5c831d57e644 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 7 Mar 2010 14:46:14 +0000 Subject: [PATCH] Clear the contents of the BBTermMemo and BBFormMemo before calling the SAT solver. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@629 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/ToSAT.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 794a833..02db33f 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -260,11 +260,13 @@ namespace BEEV { bm->GetRunTimes()->start(RunTimes::BitBlasting); - - BitBlasterNew BB(bm); - BBNodeSet set; - ASTNode BBFormula = BB.BBForm(input,set); - assert(set.size() == 0); // doesn't yet work. + ASTNode BBFormula; + { + BitBlasterNew BB(bm); + BBNodeSet set; + BBFormula = BB.BBForm(input,set); + assert(set.size() == 0); // doesn't yet work. + } bm->ASTNodeStats("after bitblasting: ", BBFormula); bm->GetRunTimes()->stop(RunTimes::BitBlasting); -- 2.47.3