projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: bc4055d)
Fixing regressions (#4189)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 31 Mar 2020 13:39:21 +0000 (08:39 -0500)
committerGitHub <noreply@github.com>
Tue, 31 Mar 2020 13:39:21 +0000 (08:39 -0500)
An option was recently deleted, forgot to disable it from a regression. Fixes a failure in regress1.

test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 patch | blob | history

diff --git a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
index 9c3fe7ac5ccf3d07e20a85add7111e7d9ef60886..471cc519bd68b5ebe6f4b5f0c7a520aa2095ae2f 100644 (file)
--- a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
+++ b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2
@@ -2,7 +2,6 @@
 (set-option :conjecture-filter-model true)
 (set-option :conjecture-gen true)
 (set-option :conjecture-no-filter true)
-(set-option :dt-ref-sk-intro true)
 (set-option :quant-ind true)
 (set-option :sygus-inference true)
 (set-info :status sat)