From 193e560ddbc02b382e016e08f9c4ef382b4c7bff Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 9 Jun 2010 13:41:37 +0000 Subject: [PATCH] bugfix. Constraints were ignored when they should have been. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@826 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 9f17113..e96696b 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -824,16 +824,16 @@ namespace BEEV //READ(Arr,index) and index is a BVCONST ASTVec c = a.GetChildren(); SortByArith(c); - FillUp_ArrReadIndex_Vec(c[0], c[1]); - ASTNode c1 = simp->SimplifyTerm(c[1]); + FillUp_ArrReadIndex_Vec(c[0], c1); + if (SYMBOL == c[0].GetKind() && bm->VarSeenInTerm(c[0], c1)) { return a; } - if (1 == TermOrder(c[0], c[1]) + if (1 == TermOrder(c[0], c1) && READ == c[0].GetKind() && bm->VarSeenInTerm(c[0][1], c1)) { -- 2.47.3