Support ackermannization on uninterpreted sorts in BV (#3372)
[cvc5.git] / test / regress / regress0 / flet2.smtv1.smt2
1 (set-option :incremental false)
2 (set-info :status sat)
3 (set-logic QF_UF)
4 (declare-sort U 0)
5 (declare-fun a () Bool)
6 (declare-fun b () Bool)
7 (check-sat-assuming ( (and (and a b) (or a b)) ))