From b04d7ee960729bcde8677be3682a2d64789f825b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 30 Mar 2011 21:53:15 +0000 Subject: [PATCH] improve recent low-coverage complaints --- test/regress/regress0/Makefile.am | 1 - test/regress/regress0/uf/Makefile.am | 1 + test/regress/regress0/uf/euf_simp09.tim.smt | 14 +++ test/regress/regress0/uf20-03.tim.cvc | 117 -------------------- test/regress/run_regression | 4 +- 5 files changed, 17 insertions(+), 120 deletions(-) create mode 100644 test/regress/regress0/uf/euf_simp09.tim.smt delete mode 100644 test/regress/regress0/uf20-03.tim.cvc diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 83291eb5a..c732ffbb2 100644 --- 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 54d89aaaa..e288a01d2 100644 --- 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 index 000000000..309090507 --- /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 index f13bdcce5..000000000 --- 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 7232fdae6..890dc438a 100755 --- 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" -- 2.30.2