From acdc5dd7650f220f360e1c5069cd8d74c9ceeb2b Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 30 May 2010 13:05:21 +0000 Subject: [PATCH] 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 --- src/simplifier/CountOfSymbols.h | 2 +- src/simplifier/bvsolver.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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()) -- 2.47.3