From b4e50806a80b8ff11e7dfa42eaac4e3b9be4b109 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 3 Oct 2010 03:42:11 +0000 Subject: [PATCH] Fix. An optimisation added in r1020 was disabled. This caused the unit tests to fail. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1025 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/simplifier.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 77d7b1b..67fe0a3 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -2644,7 +2644,7 @@ namespace BEEV output = nf->CreateTerm(BVCONCAT, inputValueWidth, t, u); } } - else if (t.GetKind() == BVCONCAT && t[0].GetKind() != BVCONCAT && false) + else if (t.GetKind() == BVCONCAT && t[0].GetKind() != BVCONCAT) { /// This makes the left hand child of every concat not a concat. -- 2.47.3