fixed proof regression script and added a new uf test case

3 files changed, 35 insertions, 5 deletions

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index bf9a36df1..19e673fea 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -42,7 +42,8 @@ TESTS =	\
 	simple.01.cvc \
 	simple.02.cvc \
 	simple.03.cvc \
-	simple.04.cvc
+	simple.04.cvc \
+	proof00.smt2
 
 EXTRA_DIST = $(TESTS) \
 	mkpidgeon
diff --git a/test/regress/regress0/uf/proof00.smt2 b/test/regress/regress0/uf/proof00.smt2
new file mode 100644
index 000000000..1b7e7b8dd
--- /dev/null
+++ b/test/regress/regress0/uf/proof00.smt2
@@ -0,0 +1,21 @@
+; PROOF
+(set-logic QF_UF)
+(set-info :source |
+CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
+ for more information. 
+
+This benchmark was obtained by trying to find a finite model of a first-order 
+formula (Albert Oliveras).
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun c3 () U)
+(declare-fun f1 (U U) U)
+(declare-fun f4 (U) U)
+(declare-fun c2 () U)
+(declare-fun c_0 () U)
+(declare-fun c_1 () U)
+(assert (let ((?v_1 (f1 c3 c_0))) (let ((?v_0 (f1 ?v_1 c_0)) (?v_2 (f1 c_0 c_0)) (?v_4 (f1 c_0 c_1)) (?v_3 (f1 ?v_1 c_1)) (?v_6 (f1 c3 c_1))) (let ((?v_5 (f1 ?v_6 c_0)) (?v_7 (f1 c_1 c_0)) (?v_9 (f1 c_1 c_1)) (?v_8 (f1 ?v_6 c_1)) (?v_10 (f4 c_0))) (let ((?v_11 (f1 c_0 ?v_10)) (?v_12 (f4 c_1))) (let ((?v_13 (f1 c_1 ?v_12)) (?v_15 (f1 c2 c_0))) (let ((?v_14 (f1 ?v_15 c_0)) (?v_16 (f1 ?v_15 c_1)) (?v_18 (f1 c2 c_1))) (let ((?v_17 (f1 ?v_18 c_0)) (?v_19 (f1 ?v_18 c_1))) (and (distinct c_0 c_1) (= (f1 ?v_0 c_0) (f1 c_0 ?v_2)) (= (f1 ?v_0 c_1) (f1 c_0 ?v_4)) (= (f1 ?v_3 c_0) (f1 c_1 ?v_2)) (= (f1 ?v_3 c_1) (f1 c_1 ?v_4)) (= (f1 ?v_5 c_0) (f1 c_0 ?v_7)) (= (f1 ?v_5 c_1) (f1 c_0 ?v_9)) (= (f1 ?v_8 c_0) (f1 c_1 ?v_7)) (= (f1 ?v_8 c_1) (f1 c_1 ?v_9)) (not (= ?v_11 (f1 ?v_10 ?v_11))) (not (= ?v_13 (f1 ?v_12 ?v_13))) (= (f1 ?v_14 c_0) (f1 (f1 ?v_2 c_0) c_0)) (= (f1 ?v_14 c_1) (f1 (f1 ?v_4 c_0) c_1)) (= (f1 ?v_16 c_0) (f1 (f1 ?v_2 c_1) c_0)) (= (f1 ?v_16 c_1) (f1 (f1 ?v_4 c_1) c_1)) (= (f1 ?v_17 c_0) (f1 (f1 ?v_7 c_0) c_0)) (= (f1 ?v_17 c_1) (f1 (f1 ?v_9 c_0) c_1)) (= (f1 ?v_19 c_0) (f1 (f1 ?v_7 c_1) c_0)) (= (f1 ?v_19 c_1) (f1 (f1 ?v_9 c_1) c_1)) (or (= ?v_2 c_0) (= ?v_2 c_1)) (or (= ?v_4 c_0) (= ?v_4 c_1)) (or (= ?v_7 c_0) (= ?v_7 c_1)) (or (= ?v_9 c_0) (= ?v_9 c_1)) (or (= ?v_10 c_0) (= ?v_10 c_1)) (or (= ?v_12 c_0) (= ?v_12 c_1)) (or (= c3 c_0) (= c3 c_1)) (or (= c2 c_0) (= c2 c_1)))))))))))
+(check-sat)
diff --git a/test/regress/run_regression b/test/regress/run_regression
index e9c17a3af..44517cc0c 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -112,7 +112,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
   proof_command='(get-proof)'
   lang=smt2
   if test -e "$benchmark.expect"; then
-    expected_proof=`grep '^% PROOF' "$benchmark.expect" &>/dev/null && echo yes`
+    expected_proof=`grep '^[%;] PROOF' "$benchmark.expect" &>/dev/null && echo yes`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -140,7 +140,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     expected_exit_status=10
     command_line=
   elif grep '^ *( *set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
-    expected_proof=
+    expected_proof=`grep '^; PROOF' "$benchmark" &>/dev/null && echo yes`
     expected_output=unsat
     expected_exit_status=20
     command_line=
@@ -276,8 +276,15 @@ fi
 
 if [ "$proof" = yes -a "$expected_proof" = yes ]; then
   gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX
-  cp "$benchmark" "$pfbenchmark";
-  echo "$proof_command" >>"$pfbenchmark";
+  # remove exit command to add proof command for smt2 benchmarks
+  if expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
+      head -n -0 "$benchmark" > "$pfbenchmark";
+      echo "$proof_command" >>"$pfbenchmark";
+      echo "(exit)" >> "$pfbenchmark";
+  else
+      cp $benchmark $pfbenchmark
+      echo "$proof_command" >>"$pfbenchmark";
+  fi
   echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`]
   time ( :; \
   ( cd `dirname "$pfbenchmark"`;
@@ -286,6 +293,7 @@ if [ "$proof" = yes -a "$expected_proof" = yes ]; then
   ) > "$outfile" 2> "$errfile" )
 
   gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX
+  
   diff --unchanged-group-format='' \
        --old-group-format='' \
        --new-group-format='%>' \