summaryrefslogtreecommitdiff
path: root/test/regress/regress0/smtlib/reset-force-logic.smt2
blob: 91aac508a4af2147a6d050f4eeb453ab2655e5ba (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

; COMMAND-LINE: --force-logic QF_LIRA
; EXPECT: sat
; EXPECT: sat

; Intentionally set the wrong logic
(set-logic QF_BV)
(declare-const x Real)
(assert (= x (- 2.5)))
(check-sat)

(reset)

; Intentionally set the wrong logic
(set-logic QF_BV)
(declare-const x Int)
(assert (= x 2))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback