From 7da35a0f1d46f01507cabe69293dee75fb7df21f Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 12 Mar 2011 23:36:07 +0000 Subject: [PATCH] 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 --- src/AST/NodeFactory/SimplifyingNodeFactory.cpp | 14 +++++++------- src/STPManager/STP.cpp | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 2339ade..cea9846 100644 --- 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 cf7d003..dd3890b 100644 --- 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 -- 2.47.3