bug fixes

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

diff --git a/src/Interpreter/mathsatinterpreter.cc b/src/Interpreter/mathsatinterpreter.cc
index ce951533e36af5d9b703c8e65d47f4c923430829..5123efef72ba932e8a0bad8d836cfe540603a6b8 100644 (file)
--- a/src/Interpreter/mathsatinterpreter.cc
+++ b/src/Interpreter/mathsatinterpreter.cc
@@ -20,7 +20,8 @@ MathSATInterpreter::MathSATInterpreter(CSolver *solver):
 }
 
 void MathSATInterpreter::compileRunCommand(char * command , size_t size){
-       snprintf(command, size, "timeout %u ./mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+       model_print("Calling MathSAT...\n");
+       snprintf(command, size, "./run.sh timeout %u mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
 MathSATInterpreter::~MathSATInterpreter(){
@@ -38,7 +39,7 @@ int MathSATInterpreter::getResult(){
                        strcpy ( cline, line.c_str() );
                        char valuestr [512];
                        uint id;
-                       if (2 == sscanf(cline,"%*[^0123456789]%u%*[^0123456789]%s", &id, valuestr)){
+                       if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)){
                                uint value;
                                if (strcmp (valuestr, "true)") == 0 ){
                                        value =1;