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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 567f6d282e12d02a172017ce0d4ca5d16a1e489c..cde63ae0f70bf9fbaca595a1b2ad960a36fbf86b 100644 (file)
--- 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 <memory>
 
 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 8d8e0ef2fe68290625a9e10e9e0eddad55dc05e7..9f59e0f455b2a5119e58be58fe9be1ac7b697fdb 100644 (file)
--- 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)