summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/issue1805.smt2
blob: 929522dec153bd53b37feae832f932ba1d51bbaf (plain) 
1
2
3
4
5
6
7
8

(set-logic AUFBVDTNIRA)
(set-info :status unsat)
(declare-fun abs1 (Int) Int)
(assert
  (forall ((x Int) (y Int))
  (! (= (<= (abs1 x) y) (and (<= (- y) x) (<= x y))) :pattern ((abs1 x) y) )))
(assert (< (abs1 (- 3)) 3))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback