is-int.smt2 « quantifiers « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

index : cvc5.git

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

git repository hosting

summary refs log tree commit diff

path: root/test/regress/regress0/quantifiers/is-int.smt2

blob: fc7fbb180dd0e5dbf350d23fa0b2db85a0ced489 (plain)

(set-logic LIRA)
(set-info :status unsat)
(assert (forall ((X Real) (Y Real)) (or (not (is_int X)) (not (>= (+ X (* (- (/ 2 3)) Y)) (- (/ 1 6)))) (not (>= (+ (* (- 1) X) (* (- (/ 1 4)) Y)) (- (/ 61 8)))) (not (>= (+ (* (- 1) X) (* (/ 5 2) Y)) 13))) ))
(check-sat)

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback