blob: df8964658b50592c32ef889b9f9e16a1c437ba0b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: sat
(set-logic UFDTSLIA)
(set-info :smt-lib-version 2.5)
(declare-datatypes () (
(Response (Response$Response (Response$Response$success Bool)))
) )
(push 1)
(declare-fun $BLout$3248$0$1$() Response)
(assert (= $BLout$3248$0$1$ (Response$Response true)))
(check-sat)
(pop 1)
(push 1)
(declare-fun $BLout$3248$2$1$() Response)
(assert (= $BLout$3248$2$1$ (Response$Response true)))
(check-sat)
|
