blob: 1e18658833cbb90c3e4e38630a8a799df5a12238 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
; SCRUBBER: sed 's/".*"/""/g'
; EXPECT: success
; EXPECT: success
; EXPECT: success
; EXPECT: success
; EXPECT: success
; EXPECT: success
; EXPECT: success
; EXPECT: (error "")
; EXPECT: (error "")
; EXPECT: (error "")
; EXPECT: (error "")
; EXPECT: (error "")
; EXPECT: success
; EXPECT: sat
(set-option :print-success true)
(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :produce-assignments true)
(set-logic UF)
(declare-fun p () Bool)
(get-unsat-core)
(get-value (p))
(get-proof)
(get-model)
(get-assignment)
(assert true)
(check-sat)
|
