summaryrefslogtreecommitdiff
path: root/test/regress/regress0/nl/issue5740-mod00.smt2
blob: e1287dacba71a0fac06e9852f453cbd1c192871a (plain) 
1
2
3
4
5
6
7

; COMMAND-LINE: --ext-rewrite-quant -q
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(define-fun f ((a Int) (b Int)) Int (ite (= b 0) 0 a))
(assert (exists ((c Int)) (distinct (f c (mod 0 0)) 0)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback