Bugfix. Substitutions need to be written through arrays too. 2/2.

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index d3ee110a9f4acfbb926b928c0bb9455fa0f34561..44afb80859e2c81d2935f0681f0a85cc846fa94e 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -792,7 +792,7 @@ namespace BEEV
 
     // Imagine in the last conjunct A is replaced by B. But there could
     // be variable A's in the first conjunct. This gets rid of 'em.
-       output = _simp->applySubstitutionMapUntilArrays(output);
+       output = _simp->applySubstitutionMap(output);
        _simp->haveAppliedSubstitutionMap();
 
     UpdateAlreadySolvedMap(_input, output);