Add order benchmark.

[satune.git] / src / Test / deserializealloytest.cc

diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc
index cef60f4c9727de506f9146300de1102ab8a53423..69c29fb0b1543def7081cc84e607fdabd7448ba7 100644 (file)
--- a/src/Test/deserializealloytest.cc
+++ b/src/Test/deserializealloytest.cc
@@ -1,14 +1,14 @@
 #include "csolver.h"
 
 
-InterpreterType getInterpreterType(char * itype){
-       if(strcmp (itype,"--alloy") == 0){
+InterpreterType getInterpreterType(char *itype) {
+       if (strcmp (itype,"--alloy") == 0) {
                return ALLOY;
-       } else if(strcmp (itype,"--z3") == 0){
+       } else if (strcmp (itype,"--z3") == 0) {
                return Z3;
-       } else if(strcmp (itype,"--smtrat") == 0){
+       } else if (strcmp (itype,"--smtrat") == 0) {
                return SMTRAT;
-       } else if(strcmp (itype,"--mathsat") == 0){
+       } else if (strcmp (itype,"--mathsat") == 0) {
                return MATHSAT;
        } else {
                printf("Unknown interpreter type: %s\n", itype);
@@ -19,14 +19,17 @@ InterpreterType getInterpreterType(char * itype){
 
 int main(int argc, char **argv) {
        printf("%d\n", argc);
-       if (argc != 2 && argc != 3) {
+       if (argc < 2 && argc > 4) {
                printf("You only specify the name of the file ...\n");
-               printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n");
+               printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat] [timeout]\n");
                exit(-1);
        }
-       CSolver *solver; 
-       if(argc == 3){
+       CSolver *solver;
+       if (argc >= 3) {
                solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));
+               if (argc == 4) {
+                       solver->setSatSolverTimeout(atol(argv[3]));
+               }
        } else {
                solver = CSolver::deserialize(argv[1]);
        }