set(regress_0_tests
regress0/arith/ackermann.real.smt2
+ regress0/arith/arith-eq.smt2
+ regress0/arith/arith-mixed.smt2
+ regress0/arith/arith-tighten-1.smt2
+ regress0/arith/arith-strict.smt2
+ regress0/arith/arith-mixed-types-tighten.smt2
+ regress0/arith/arith-mixed-types-no-tighten.smt2
regress0/arith/arith.01.cvc
regress0/arith/arith.02.cvc
regress0/arith/arith.03.cvc
--- /dev/null
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LRA)
+
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+
+(assert (= z 0))
+(assert (= (* 3 x) y))
+(assert (= (+ 1 (* 5 x)) y))
+(assert (= (+ 7 (* 4 x)) y))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LIRA)
+
+(declare-fun x () Real)
+(declare-fun n () Int)
+
+; Even though `n` is an integer, this would be UNSAT for real `n`, so the integrality can be ignored.
+(assert
+ (and
+ (>= (+ x n) 1)
+ (<= n 0)
+ (<= x 0)
+ )
+)
+
+(check-sat)
+
--- /dev/null
+; COMMAND-LINE: --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_LIRA)
+
+(declare-fun x_44 () Real)
+(declare-fun x_45 () Real)
+
+; This test is a subset of one of the `../lemmas` tests. I think `../lemmas/sc_init_frame_gap.induction.smtv1.smt2`.
+(declare-fun termITE_30 () Int)
+(declare-fun termITE_3 () Real)
+(declare-fun termITE_4 () Real)
+(declare-fun termITE_8 () Real)
+(declare-fun termITE_9 () Real)
+(declare-fun termITE_31 () Int)
+
+(assert
+ (let ((_let_0 (* (- 1.0) termITE_3)))
+ (and
+ (>= (+ termITE_8 (* (- 1.0) termITE_9)) 0.0)
+ ; This literal can be tightened to `termITE_31 <= 1`.
+ (not (>= termITE_31 2))
+ (>= (+ (* (- 1.0) x_44) (/ termITE_31 1)) 0.0)
+ (>= (+ x_44 (* (- 1.0) termITE_4)) 0.0)
+ (not (>= (+ _let_0 (* (/ 1 2) termITE_8)) 0.0))
+ (>= (+ (* (- 1.0) x_45) termITE_9) 0.0)
+ (>= (+ x_45 (/ (* (- 1) termITE_30) 1)) 0.0)
+ (>= termITE_30 2)
+ (>= (+ _let_0 termITE_4) 0.0)))
+)
+
+(check-sat)
+