Bugfix. The same index could be stored twice in the array. I suspect it used to cause...

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 9cc8437464edd2178ab1d58f5559fc057aaf1daf..90f64bfb1c223bb74daf99f5b079bbeb99bd8c37 100644 (file)
--- 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 =