summaryrefslogtreecommitdiff
path: root/test/regress/regress0/nl/issue3959.smt2
blob: eccd6b3015858c873a82228f62f4a70c6f091d52 (plain) 
1
2
3
4
5
6
7
8
9
10
11

; COMMAND-LINE: --produce-unsat-cores --incremental
; EXPECT: sat

; Note: the logic must include UF to trigger the bug
(set-logic QF_UFNIA)
(declare-const v10 Bool)
(declare-const i12 Int)
(declare-const i16 Int)
(push 1)
(assert (=> (<= (mod i12 38) i16) v10))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback