projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 4125891)
Fix (#3530)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 4 Dec 2019 22:43:02 +0000 (16:43 -0600)
committerGitHub <noreply@github.com>
Wed, 4 Dec 2019 22:43:02 +0000 (16:43 -0600)
test/regress/regress1/sygus/issue3514.smt2 patch | blob | history

diff --git a/test/regress/regress1/sygus/issue3514.smt2 b/test/regress/regress1/sygus/issue3514.smt2
index dd6011df92a3702347074d06f3c9e58834df80da..c643e7d5ade9a5ddd537abd325cc0a9a9192eddb 100644 (file)
--- a/test/regress/regress1/sygus/issue3514.smt2
+++ b/test/regress/regress1/sygus/issue3514.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference
+; COMMAND-LINE: --sygus-inference --no-check-models
 (set-logic ALL)
 (assert
  (forall ((a Real))