Adding SMTRat and MathSAT interpreters

[satune.git] / src / Interpreter / smtinterpreter.cc

diff --git a/src/Interpreter/smtinterpreter.cc b/src/Interpreter/smtinterpreter.cc
index dc8f1cdb9e199c90fb00a868b80e5339fafea626..82c887b244afa77156e97461382af4c395dc3a06 100644 (file)
--- a/src/Interpreter/smtinterpreter.cc
+++ b/src/Interpreter/smtinterpreter.cc
@@ -15,9 +15,6 @@
 
 using namespace std;
 
 
 using namespace std;
 

-#define SMTFILENAME "satune.smt"
-#define SMTSOLUTIONFILE "solution.sol"
-

 SMTInterpreter::SMTInterpreter(CSolver *_solver): 
        Interpreter(_solver) 
 {
 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("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];
                        string valueline;
                        ASSERT(getline(input, valueline));
                        char cline [line.size()+1];