From: Andrew Reynolds Date: Tue, 31 Mar 2020 13:39:21 +0000 (-0500) Subject: Fixing regressions (#4189) X-Git-Tag: cvc5-1.0.0~3422 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=501894d709c19aebcaed1bd43e506501a8bbd69b;p=cvc5.git Fixing regressions (#4189) An option was recently deleted, forgot to disable it from a regression. Fixes a failure in regress1. --- diff --git a/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 b/test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 index 9c3fe7ac5..471cc519b 100644 --- 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)