X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FInterpreter%2Fsmtinterpreter.cc;h=82c887b244afa77156e97461382af4c395dc3a06;hp=dc8f1cdb9e199c90fb00a868b80e5339fafea626;hb=b170f31ca9df1c465adec1c156c5a8b1aa49a3c0;hpb=4c58af641a877bb6d65769994c8fd57ecedbd22c

diff --git a/src/Interpreter/smtinterpreter.cc b/src/Interpreter/smtinterpreter.cc
index dc8f1cd..82c887b 100644
--- a/src/Interpreter/smtinterpreter.cc
+++ b/src/Interpreter/smtinterpreter.cc
@@ -15,9 +15,6 @@
 
 using namespace std;
 
-#define SMTFILENAME "satune.smt"
-#define SMTSOLUTIONFILE "solution.sol"
-
 SMTInterpreter::SMTInterpreter(CSolver *_solver): 
 	Interpreter(_solver) 
 {
@@ -82,7 +79,7 @@ int SMTInterpreter::getResult(){
 		if(line.find("unsat")!= line.npos){
 			return IS_UNSAT;
 		}
-		if(line.find("(define-fun") != line.npos){
+		if(line.find("(define-fun") != line.npos || line.find("( (") != line.npos){
 			string valueline;
 			ASSERT(getline(input, valueline));
 			char cline [line.size()+1];