blob: 489d686b3a2e901b730d649be06e6670cd6ef28c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.")
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
; EXPECT-ERROR: Expected result unsat but got sat
; ERROR-SCRUBBER: sed -e '/Fatal failure within.*/d'
; EXIT: -6
(set-option :incremental true)
(set-option :produce-unsat-cores true)
(set-logic QF_BV)
(set-info :status unsat)
(get-unsat-core)
(set-info :status sat)
(check-sat)
(set-info :status sat)
(check-sat)
(push)
(assert false)
(check-sat)
(pop)
(set-info :status unsat)
(check-sat)
|
