blob: dd4e9ea0912d20a608a3249f4bde7be3371dfc27 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
; COMMAND-LINE: --incremental
; EXPECT: sat
; EXPECT: sat
(set-logic UFDTSLIA)
(set-info :smt-lib-version 2.6)
(declare-datatype 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)
|
