summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers/issue5484-qe.smt2
blob: 9fcc7dcba46738293a5528705a2f6d1c115dde55 (plain)
1
2
3
4
5
6
7
8
9
10
; COMMAND-LINE: -q
; SCRUBBER: sed 's/(.*)/()/g'
; EXPECT: ()
; EXIT: 0
(set-logic NIA)
(declare-fun v9 () Bool)
(declare-fun v18 () Bool)
(declare-fun i2 () Int)
(declare-fun v31 () Bool)
(get-qe (forall ((q23 Int) (q24 Int) (q25 Int) (q26 Int) (q27 Bool) (q28 Int) (q29 Int)) (xor (=> (not (not (distinct 83 407))) (> (- i2 31 722) 319)) (forall ((q23 Int) (q24 Int) (q25 Int) (q26 Int) (q27 Bool) (q28 Int) (q29 Int)) (not (not (not v9)))) v31 (> 665 (+ (mod 83 923) (div i2 850)) 319 (- 939 878)) v18)))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback