Fix the method to count the number of instances in an expression. Previously it was...

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

diff --git a/src/simplifier/CountOfSymbols.h b/src/simplifier/CountOfSymbols.h
index 244e44ad13f8ede0dbceeb44a5104ba835a6e272..3c10ab0332763140de1bf14476c2be7c6732cf3d 100644 (file)
--- a/src/simplifier/CountOfSymbols.h
+++ b/src/simplifier/CountOfSymbols.h
@@ -42,7 +42,7 @@ class CountOfSymbols {
                case SYMBOL:
                        //cerr << "debugging: symbol added: " << term << endl;
                        Vars[term]++;
-                       break;
+                       return;
                case READ:
                        //skip the arrayname, provided the arrayname is a SYMBOL
                        //But we don't skip it if it's a WRITE function??

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 76e009806330197b0c392cc3e743ce856aa2716f..e0a80f6d3541d09c45667b51cae5fb2fc8839af5 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -202,7 +202,7 @@ namespace BEEV
       case SYMBOL:
         //cerr << "debugging: symbol added: " << term << endl;
         Vars.insert(term);
-        break;
+        return;
       case READ:
         //skip the arrayname, provided the arrayname is a SYMBOL
         if (SYMBOL == term[0].GetKind())