summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers/issue4062-cegqi-aux.smt2
blob: 0296c978cd68f96f83853c1dd3691d924d6debb2 (plain) 
1
2
3
4
5
6
7
8
9

; COMMAND-LINE: --arith-rewrite-equalities --global-negate --no-check-models
; EXPECT: sat
(set-logic NIA)
(set-option :arith-rewrite-equalities true)
(set-option :global-negate true)
(set-info :status sat)
(declare-const i5 Int)
(assert (= 562 (abs i5)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback