projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 25ee78e)
Minor fixes to regressions (#3702)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 3 Feb 2020 21:05:45 +0000 (15:05 -0600)
committerGitHub <noreply@github.com>
Mon, 3 Feb 2020 21:05:45 +0000 (13:05 -0800)
Fixes two issues in regressions, fixes regress1.

test/regress/regress0/sygus/pbe-pred-contra.sy patch | blob | history
test/regress/regress1/nl/issue3617.smt2 patch | blob | history

diff --git a/test/regress/regress0/sygus/pbe-pred-contra.sy b/test/regress/regress0/sygus/pbe-pred-contra.sy
index 22fc12e60a9bf1142d9722d327abf5f8c938d92a..5fbe91e2eb0acbc71a99cffe904fe8d33bb13f03 100644 (file)
--- a/test/regress/regress0/sygus/pbe-pred-contra.sy
+++ b/test/regress/regress0/sygus/pbe-pred-contra.sy
@@ -1,4 +1,4 @@
-; COMMAND_LINE: --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 ; EXPECT: unknown
 (set-logic LIA)
 (synth-fun P ((x Int)) Bool)
diff --git a/test/regress/regress1/nl/issue3617.smt2 b/test/regress/regress1/nl/issue3617.smt2
index cd96d536a7bf117391f400a27bb20e38faacc559..149b6a535a7cdd00c8df1aa81e862e476bce77fc 100644 (file)
--- a/test/regress/regress1/nl/issue3617.smt2
+++ b/test/regress/regress1/nl/issue3617.smt2
@@ -8,4 +8,3 @@
 )
 (assert (> a 0))
 (check-sat)
-(get-model)