From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 3 Feb 2020 21:05:45 +0000 (-0600)
Subject: Minor fixes to regressions (#3702)
X-Git-Tag: cvc5-1.0.0~3690
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c55227e6ef30149e6a008fdea56573f67244a61;p=cvc5.git

Minor fixes to regressions (#3702)

Fixes two issues in regressions, fixes regress1.
---

diff --git a/test/regress/regress0/sygus/pbe-pred-contra.sy b/test/regress/regress0/sygus/pbe-pred-contra.sy
index 22fc12e60..5fbe91e2e 100644
--- 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 cd96d536a..149b6a535 100644
--- 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)