test/regress/regress0/issue5540-model-decls.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

; SCRUBBER: sed -e 's/Bool.*$/Bool/'
; COMMAND-LINE: --dump-models -i
; EXPECT:sat
; EXPECT: (
; EXPECT: (define-fun a () Bool
; EXPECT: )
; EXPECT: sat
; EXPECT: (
; EXPECT: (define-fun a () Bool
; EXPECT: )
; EXPECT: sat
; EXPECT: (
; EXPECT: (define-fun a () Bool
; EXPECT: )
(set-logic ALL)
(declare-fun a () Bool)
(check-sat)
(check-sat)
(check-sat)