From 501894d709c19aebcaed1bd43e506501a8bbd69b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 31 Mar 2020 08:39:21 -0500 Subject: [PATCH] Fixing regressions (#4189) 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 | 1 - 1 file changed, 1 deletion(-) 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) -- 2.30.2