Fix. Missing break; in a switch. Dumb luck meant it didn't cause any problems.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1204 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 2339adefe29e34403544073ea78d6b95c79083c1..cea9846afbed84fcf5a2a17088340bddd091541b 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -467,12 +467,15 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
        switch (kind)
        {
        case BEEV::ITE:
+       {
                if (children[0]== ASTTrue)
                        result = children[1];
-               if (children[0]== ASTFalse)
+               else if (children[0]== ASTFalse)
                        result = children[2];
-
-
+               else if (children[1] == children[2])
+                       result = children[1];
+               break;
+       }
 
        case BEEV::BVNEG:
        {
@@ -484,18 +487,15 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
                        break;
                default: // quieten compiler.
                        break;
-
                }
        }
-               break;
+       break;
        default: // quieten compiler.
                break;
-
        }
 
        if (result.IsNull())
                result = hashing.CreateTerm(kind, width, children);
 
        return result;
-
 }

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index cf7d0031711cc132cbb15a198e3ad1f59b7a09a0..dd3890be0ca6b04958341d16e90d1271f07d8efb 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -371,7 +371,7 @@ namespace BEEV {
 
 
     bool optimize_enabled = bm->UserFlags.optimize_flag;
-    if (final_difficulty_score > 1.1 *initial_difficulty_score  && !arrayops)
+    if (final_difficulty_score > 1.1 *initial_difficulty_score  && !arrayops && bm->UserFlags.isSet("difficulty-reversion","1"))
     {
        // If the simplified problem is harder, than the
        // initial problem we revert back to the initial