Set assertion in `CnfStream::ensureLiteral()` (#3927)
[cvc5.git] / test / regress / regress0 / opt-abd-no-use.smt2
1 (set-logic QF_LIA)
2 (set-info :status sat)
3 (set-option :produce-abducts true)
4 (declare-fun x () Int)
5 (assert (> x 0))
6 (check-sat)