improve recent low-coverage complaints

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 83291eb5aa21d8771322bdba2819a465abc5e231..c732ffbb287120a06ed85cf987cea5ad2f48f618 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -52,7 +52,6 @@ CVC_TESTS = \
        test9.cvc \
        test11.cvc \
        uf20-03.cvc \
-       uf20-03.tim.cvc \
        wiki.01.cvc \
        wiki.02.cvc \
        wiki.03.cvc \

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 54d89aaaa400a8e4fc5429c101969db0051fbe8f..e288a01d2544ec38a6b37c940c304bad1d265f86 100644 (file)
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -12,6 +12,7 @@ TESTS =       \
        euf_simp06.smt \
        euf_simp08.smt \
        euf_simp09.smt \
+       euf_simp09.tim.smt \
        euf_simp10.smt \
        euf_simp11.smt \
        euf_simp12.smt \

diff --git a/test/regress/regress0/uf/euf_simp09.tim.smt b/test/regress/regress0/uf/euf_simp09.tim.smt
new file mode 100644 (file)
index 0000000..3090905
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp09.tim.smt
@@ -0,0 +1,14 @@
+% COMMAND-LINE: --uf tim
+% EXPECT: unsat
+% EXIT: 20
+(benchmark euf_simp9.smt
+
+  :status unsat
+  :difficulty { unknown }
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (A)
+  :extrafuns ((x A))
+  :extrafuns ((f A A))
+  :formula (let (?cvc_1 (f (f x))) (let (?cvc_0 (f (f ?cvc_1))) (not (implies (and (= ?cvc_0 x) (= (f (f ?cvc_0)) x)) (= ?cvc_1 x)))))
+)

diff --git a/test/regress/regress0/uf20-03.tim.cvc b/test/regress/regress0/uf20-03.tim.cvc
deleted file mode 100644 (file)
index f13bdcc..0000000
--- a/test/regress/regress0/uf20-03.tim.cvc
+++ /dev/null
@@ -1,117 +0,0 @@
-% COMMAND-LINE: --uf=tim
-% EXPECT: invalid
-x_1 : BOOLEAN;
-x_2 : BOOLEAN;
-x_3 : BOOLEAN;
-x_4 : BOOLEAN;
-x_5 : BOOLEAN;
-x_6 : BOOLEAN;
-x_7 : BOOLEAN;
-x_8 : BOOLEAN;
-x_9 : BOOLEAN;
-x_10 : BOOLEAN;
-x_11 : BOOLEAN;
-x_12 : BOOLEAN;
-x_13 : BOOLEAN;
-x_14 : BOOLEAN;
-x_15 : BOOLEAN;
-x_16 : BOOLEAN;
-x_17 : BOOLEAN;
-x_18 : BOOLEAN;
-x_19 : BOOLEAN;
-x_20 : BOOLEAN;
-ASSERT NOT x_9 OR x_3 OR NOT x_15;
-ASSERT NOT x_12 OR NOT x_4 OR NOT x_15;
-ASSERT x_6 OR x_14 OR NOT x_17;
-ASSERT x_10 OR x_16 OR x_11;
-ASSERT NOT x_15 OR x_20 OR NOT x_7;
-ASSERT NOT x_1 OR x_10 OR x_16;
-ASSERT x_13 OR x_17 OR NOT x_7;
-ASSERT NOT x_2 OR NOT x_14 OR NOT x_13;
-ASSERT x_13 OR NOT x_6 OR x_15;
-ASSERT NOT x_9 OR x_3 OR x_16;
-ASSERT NOT x_20 OR NOT x_13 OR x_4;
-ASSERT NOT x_7 OR x_15 OR NOT x_14;
-ASSERT NOT x_15 OR NOT x_16 OR x_6;
-ASSERT x_5 OR NOT x_18 OR x_20;
-ASSERT NOT x_16 OR NOT x_19 OR x_7;
-ASSERT x_20 OR NOT x_18 OR NOT x_2;
-ASSERT x_10 OR NOT x_19 OR NOT x_14;
-ASSERT x_16 OR NOT x_7 OR x_12;
-ASSERT x_6 OR NOT x_5 OR NOT x_1;
-ASSERT NOT x_9 OR x_11 OR x_15;
-ASSERT x_19 OR NOT x_6 OR x_7;
-ASSERT NOT x_11 OR x_17 OR NOT x_19;
-ASSERT x_9 OR NOT x_16 OR x_6;
-ASSERT x_15 OR NOT x_20 OR x_10;
-ASSERT x_9 OR NOT x_1 OR NOT x_11;
-ASSERT NOT x_8 OR NOT x_19 OR x_5;
-ASSERT NOT x_19 OR x_11 OR x_20;
-ASSERT NOT x_12 OR x_13 OR NOT x_3;
-ASSERT NOT x_7 OR NOT x_17 OR NOT x_19;
-ASSERT x_17 OR x_6 OR NOT x_11;
-ASSERT NOT x_7 OR NOT x_17 OR x_10;
-ASSERT NOT x_14 OR x_9 OR x_20;
-ASSERT x_1 OR NOT x_18 OR NOT x_16;
-ASSERT NOT x_2 OR NOT x_15 OR x_20;
-ASSERT x_14 OR x_18 OR NOT x_1;
-ASSERT NOT x_8 OR NOT x_4 OR x_1;
-ASSERT x_13 OR x_3 OR NOT x_9;
-ASSERT x_5 OR x_7 OR x_8;
-ASSERT x_9 OR x_4 OR NOT x_20;
-ASSERT NOT x_18 OR NOT x_15 OR NOT x_10;
-ASSERT x_10 OR x_3 OR NOT x_20;
-ASSERT x_20 OR NOT x_14 OR x_16;
-ASSERT x_20 OR NOT x_3 OR NOT x_11;
-ASSERT NOT x_12 OR x_19 OR NOT x_16;
-ASSERT NOT x_3 OR x_5 OR x_10;
-ASSERT x_8 OR x_13 OR NOT x_7;
-ASSERT NOT x_2 OR NOT x_15 OR x_10;
-ASSERT NOT x_3 OR x_9 OR x_16;
-ASSERT NOT x_12 OR NOT x_16 OR NOT x_18;
-ASSERT x_3 OR x_1 OR NOT x_12;
-ASSERT NOT x_18 OR x_13 OR x_5;
-ASSERT x_1 OR x_3 OR NOT x_19;
-ASSERT NOT x_19 OR NOT x_5 OR x_6;
-ASSERT NOT x_20 OR x_8 OR NOT x_2;
-ASSERT x_17 OR NOT x_8 OR NOT x_13;
-ASSERT x_7 OR NOT x_11 OR NOT x_12;
-ASSERT NOT x_10 OR NOT x_14 OR NOT x_20;
-ASSERT NOT x_1 OR x_16 OR NOT x_12;
-ASSERT x_5 OR NOT x_3 OR x_9;
-ASSERT NOT x_18 OR x_8 OR x_14;
-ASSERT x_1 OR x_16 OR x_12;
-ASSERT x_20 OR NOT x_1 OR NOT x_16;
-ASSERT x_5 OR x_10 OR NOT x_13;
-ASSERT x_9 OR NOT x_10 OR x_6;
-ASSERT NOT x_12 OR x_10 OR NOT x_14;
-ASSERT NOT x_13 OR x_1 OR x_4;
-ASSERT NOT x_20 OR NOT x_7 OR x_3;
-ASSERT x_12 OR x_1 OR NOT x_10;
-ASSERT NOT x_1 OR NOT x_16 OR x_7;
-ASSERT x_11 OR NOT x_6 OR NOT x_4;
-ASSERT x_1 OR x_16 OR NOT x_20;
-ASSERT x_9 OR x_7 OR x_15;
-ASSERT NOT x_6 OR x_17 OR x_10;
-ASSERT x_8 OR x_9 OR x_17;
-ASSERT x_18 OR x_11 OR x_10;
-ASSERT x_7 OR x_1 OR NOT x_8;
-ASSERT NOT x_5 OR NOT x_12 OR x_18;
-ASSERT NOT x_6 OR x_2 OR x_15;
-ASSERT x_2 OR x_18 OR x_1;
-ASSERT NOT x_7 OR NOT x_13 OR x_16;
-ASSERT x_18 OR x_19 OR x_9;
-ASSERT x_9 OR NOT x_14 OR x_18;
-ASSERT x_14 OR x_12 OR NOT x_5;
-ASSERT NOT x_13 OR NOT x_7 OR NOT x_14;
-ASSERT NOT x_1 OR x_8 OR NOT x_16;
-ASSERT NOT x_11 OR x_4 OR x_7;
-ASSERT NOT x_4 OR x_20 OR x_5;
-ASSERT NOT x_5 OR x_2 OR x_12;
-ASSERT NOT x_5 OR x_13 OR NOT x_18;
-ASSERT NOT x_18 OR x_9 OR x_1;
-ASSERT x_10 OR NOT x_11 OR x_16;
-
-
-QUERY FALSE;
-% EXIT: 10

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 7232fdae6886e92a63b6ac4ce2c8e835e6fd75d8..890dc438a1f270ce40c465a11ba69865c0b39bcb 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -62,7 +62,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
     # this frustrates our auto-language-detection, so add explicit --lang
     gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX
-    command_line="${command_line:+ $command_line}--lang=smt"
+    command_line="${command_line:+$command_line }--lang=smt"
     grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
@@ -96,7 +96,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
     # this frustrates our auto-language-detection, so add explicit --lang
     gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX
-    command_line="${command_line:+ $command_line}--lang=smt2"
+    command_line="${command_line:+$command_line }--lang=smt2"
     grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"