From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 18 Jan 2011 12:45:56 +0000 (+0000)
Subject: Bugfix. The same index could be stored twice in the array. I suspect it used to cause... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ee791225977dd3e2961a12c372f36e71acf2d124;p=francis%2Fstp.git

Bugfix. The same index could be stored twice in the array. I suspect it used to cause problems. But don't have any fixed test cases to prove it.

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

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index 9cc8437..90f64bf 100644
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -88,14 +88,15 @@ namespace BEEV
               {
             	const ASTNode& index_j = listOfIndices[j];
 
-            	// We assume there are no duplicate constant indexes in the list of readindexes,
-            	// so "i" and "j" will never be equal.
-            	if (BVCONST == index_i.GetKind() && index_j.GetKind() == BVCONST)
+            	// If the index is a constant, and different, then there's no reason to check.
+            	// Sometimes we get the same index stored multiple times in the array. Not sure why...
+            	if (BVCONST == index_i.GetKind() && index_j.GetKind() == BVCONST && index_i != index_j)
             	{
             		assert(index_i != index_j);
             		continue;
             	}
 
+
                 //prepare for SAT LOOP
                 //first construct the antecedent for the LA axiom
                 ASTNode eqOfIndices =