From d13b1d3ed414551194d343adfcbb18e782e00d12 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 15 Jun 2012 14:40:15 +0000 Subject: [PATCH] Fix the build. Remove code I didn't mean to checkin. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1666 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 6 ------ src/absrefine_counterexample/CounterExample.cpp | 4 ++-- 2 files changed, 2 insertions(+), 8 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 567f6d2..cde63ae 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -23,7 +23,6 @@ #include "../simplifier/UseITEContext.h" #include "../simplifier/AlwaysTrue.h" #include "../simplifier/AIGSimplifyPropositionalCore.h" -#include "../simplifier/TransformExtensionality.h" #include namespace BEEV { @@ -82,11 +81,6 @@ namespace BEEV { NewSolver.setSeed(bm->UserFlags.random_seed); } - TransformExtensionality t(bm); - original_input = t.topLevel(original_input); - - - SOLVER_RETURN_TYPE result; result = TopLevelSTPAux(NewSolver, original_input); diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 8d8e0ef..9f59e0f 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -955,8 +955,8 @@ namespace BEEV // invalid if (ASTTrue == orig_result) { - //if (bm->UserFlags.check_counterexample_flag) - // CheckCounterExample(SatSolver.okay()); + if (bm->UserFlags.check_counterexample_flag) + CheckCounterExample(SatSolver.okay()); if (bm->UserFlags.stats_flag || bm->UserFlags.print_counterexample_flag) -- 2.47.3