projects
/
satune.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Adding SMTRat and MathSAT interpreters
[satune.git]
/
src
/
Interpreter
/
interpreter.cc
diff --git
a/src/Interpreter/interpreter.cc
b/src/Interpreter/interpreter.cc
index d87cbd9fbad083de008e8f82a9ce656c82ffc9cd..a5927f71d037ce31dcf03f57356a5b3fddf543d5 100644
(file)
--- a/
src/Interpreter/interpreter.cc
+++ b/
src/Interpreter/interpreter.cc
@@
-56,9
+56,12
@@
int Interpreter::solve(){
}
compileRunCommand(buffer, sizeof(buffer));
int status = system(buffer);
}
compileRunCommand(buffer, sizeof(buffer));
int status = system(buffer);
- if (status == 0
) {
+ if (status == 0
|| status == 512 ) { //For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
//Read data in from results file
result = getResult();
//Read data in from results file
result = getResult();
+ } else {
+ model_print("Error in running command<returned %d>: %s\n", status, buffer);
+ exit(-1);
}
return result;
}
}
return result;
}