test/regress/regress2/sygus/issue4022-conjecture-gen.smt2


1
2
3
4
5
6
7
8
9
10
11

(set-logic ALL)
(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)
(declare-fun a (Int) Bool)
(assert (exists ((b Int)) (a b)))
(check-sat)