projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 136617c)
Fix annotations in regress2. (#1917)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 15 May 2018 03:25:40 +0000 (22:25 -0500)
committerGitHub <noreply@github.com>
Tue, 15 May 2018 03:25:40 +0000 (22:25 -0500)
test/regress/regress2/sygus/sixfuncs.sy patch | blob | history
test/regress/regress2/sygus/vcb.sy patch | blob | history

diff --git a/test/regress/regress2/sygus/sixfuncs.sy b/test/regress/regress2/sygus/sixfuncs.sy
index 5280ffb2063b70db0503da98f8077a511902c277..fc4d7e5bed26649453f6043b44c83b9f21574a08 100644 (file)
--- 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 9cc2389f3c9a485bd5c0ba0f9ff86c92f50b468d..7f895fae41ce3d520c5ad0c3508567964d6929ca 100644 (file)
--- 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)