From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 15 May 2018 03:25:40 +0000 (-0500)
Subject: Fix annotations in regress2. (#1917)
X-Git-Tag: cvc5-1.0.0~5051
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc936567859cf1ebae52ede50a95cdb8e31a999e;p=cvc5.git

Fix annotations in regress2. (#1917)
---

diff --git a/test/regress/regress2/sygus/sixfuncs.sy b/test/regress/regress2/sygus/sixfuncs.sy
index 5280ffb20..fc4d7e5be 100644
--- a/test/regress/regress2/sygus/sixfuncs.sy
+++ b/test/regress/regress2/sygus/sixfuncs.sy
@@ -1,3 +1,5 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f1 ((p1 Int) (P1 Int)) Int
diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy
index 9cc2389f3..7f895fae4 100644
--- a/test/regress/regress2/sygus/vcb.sy
+++ b/test/regress/regress2/sygus/vcb.sy
@@ -1,3 +1,5 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f1 ((x1 Int) (x2 Int)) Int)
@@ -51,4 +53,4 @@
 
 (constraint (or (Bad x1 x2) (not (AllZero (f1 x1 x2) (f2 x1 x2)))))
 
-(check-synth)
\ No newline at end of file
+(check-synth)