From: trevor_hansen Date: Thu, 14 Apr 2011 05:32:21 +0000 (+0000) Subject: Shortcut in a rare circumstance. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=2108e420197d13b1d65dd555defe696d25fce3b6;p=francis%2Fstp.git Shortcut in a rare circumstance. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1276 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index d8e7ba2..332fd69 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -561,6 +561,12 @@ namespace BEEV if (ASTFalse == cond) continue; + if (ASTTrue == cond) + { + result = it2->second.ite; + break; + } + result = simp->CreateSimplifiedTermITE(cond, it2->second.ite, result); }