From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 30 May 2010 13:05:21 +0000 (+0000)
Subject: Fix the method to count the number of instances in an expression. Previously it was... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=acdc5dd7650f220f360e1c5069cd8d74c9ceeb2b;p=francis%2Fstp.git

Fix the method to count the number of instances in an expression. Previously it was counting no more than one.



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 244e44a..3c10ab0 100644
--- 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 76e0098..e0a80f6 100644
--- 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())