blob: 91fe27b0b3a8f807a1f3e3447f6431c31002545a (
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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SAT)
(define-fun
__node_init_top_0 (
(top.usr.OK_a_0 Bool)
(top.res.init_flag_a_0 Bool)
) Bool
(and (= top.usr.OK_a_0 true) top.res.init_flag_a_0)
)
(define-fun
__node_trans_top_0 (
(top.usr.OK_a_1 Bool)
(top.res.init_flag_a_1 Bool)
(top.usr.OK_a_0 Bool)
(top.res.init_flag_a_0 Bool)
) Bool
(and (= top.usr.OK_a_1 true) (not top.res.init_flag_a_1))
)
(synth-inv str_invariant(
(top.usr.OK Bool)
(top.res.init_flag Bool)
))
(define-fun
init (
(top.usr.OK Bool)
(top.res.init_flag Bool)
) Bool
(and (= top.usr.OK true) top.res.init_flag)
)
(define-fun
trans (
;; Current state.
(top.usr.OK Bool)
(top.res.init_flag Bool)
;; Next state.
(top.usr.OK! Bool)
(top.res.init_flag! Bool)
) Bool
(and (= top.usr.OK! true) (not top.res.init_flag!))
)
(define-fun
prop (
(top.usr.OK Bool)
(top.res.init_flag Bool)
) Bool
top.usr.OK
)
(inv-constraint str_invariant init trans prop)
(check-synth)
|
