Fix. The last revision has some debugging messages enabled. Ooops.

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

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index a7935c60486f39aa745db816a03e8a94dc13e3c2..657f27815fbbf309f7d5db07159329d843102cfa 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -16,7 +16,7 @@ namespace BEEV {
 class Simplifier;
 class ArrayTransformer;
 
-const bool debug_substn = true;
+const bool debug_substn = false;
 
 class SubstitutionMap {
 

diff --git a/src/simplifier/VariablesInExpression.cpp b/src/simplifier/VariablesInExpression.cpp
index 36ecc2c67090f0264b8875f25d47ca6c3f2b5063..278b2c6f48cc9c2a76a0b4be4fb974a23c731f9c 100644 (file)
--- a/src/simplifier/VariablesInExpression.cpp
+++ b/src/simplifier/VariablesInExpression.cpp
@@ -158,7 +158,7 @@ bool VariablesInExpression::VarSeenInTerm(const ASTNode& var,
                                continue;
 
                        const ASTNodeSet& sym = *TermsAlreadySeenMap.find(av[i])->second;
-                       cout << "set: " << i << " " << sym.size() << endl;
+                       //cout << "set: " << i << " " << sym.size() << endl;
                        symbols->insert(sym.begin(), sym.end());
                }
                TermsAlreadySeenMap.insert(make_pair(symbol_graph[term.GetNodeNum()], symbols));