X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FInterpreter%2Fmathsatinterpreter.cc;h=5123efef72ba932e8a0bad8d836cfe540603a6b8;hb=88522b82efee075d4dbaf75e82231a399bcbb41c;hp=ce951533e36af5d9b703c8e65d47f4c923430829;hpb=e9ca288c7f0cf0f3bb9508c3cc9b212f557bcc40;p=satune.git

diff --git a/src/Interpreter/mathsatinterpreter.cc b/src/Interpreter/mathsatinterpreter.cc
index ce95153..5123efe 100644
--- 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;