From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 Dec 2019 22:43:02 +0000 (-0600)
Subject: Fix (#3530)
X-Git-Tag: cvc5-1.0.0~3800
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1741bb48e54f25ef4fd7776380deca1dd60a2201;p=cvc5.git

Fix (#3530)
---

diff --git a/test/regress/regress1/sygus/issue3514.smt2 b/test/regress/regress1/sygus/issue3514.smt2
index dd6011df9..c643e7d5a 100644
--- 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))