Set assertion in `CnfStream::ensureLiteral()` (#3927)
[cvc5.git] / test / regress / regress0 / parallel-let.smt2
1 (set-logic QF_UF)
2 (set-info :status unsat)
3 (declare-sort U 0)
4 (declare-fun x () U)
5 (declare-fun y () U)
6 (assert (distinct x y))
7 (assert (let ((x y) (y x)) (= x y)))
8 (check-sat)
9 (exit)