-
Notifications
You must be signed in to change notification settings - Fork 24
/
sygus-bench-101.c.smt
73 lines (72 loc) · 3.16 KB
/
sygus-bench-101.c.smt
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
70
71
72
(set-info :original "/tmp/sea-GSofud/101.pp.ms.o.bc")
(set-info :authors "SeaHorn v.0.1.0-rc3")
(declare-rel verifier.error (Bool Bool Bool ))
(declare-rel main@entry (Int ))
(declare-rel main@_bb (Int Int ))
(declare-rel main@verifier.error.split ())
(declare-var main@%_9_0 Bool )
(declare-var main@%_10_0 Bool )
(declare-var main@%or.cond.i_0 Bool )
(declare-var main@%_11_0 Bool )
(declare-var main@%_5_0 Bool )
(declare-var main@%_0_0 Int )
(declare-var @unknown_0 Int )
(declare-var main@%_2_0 Int )
(declare-var main@entry_0 Bool )
(declare-var main@%_1_0 Int )
(declare-var main@_bb_0 Bool )
(declare-var main@%x.0.i_0 Int )
(declare-var main@%x.0.i_1 Int )
(declare-var main@_bb1_0 Bool )
(declare-var main@%_7_0 Int )
(declare-var main@_bb_1 Bool )
(declare-var main@%x.0.i_2 Int )
(declare-var main@_bb2_0 Bool )
(declare-var main@_bb3_0 Bool )
(declare-var main@verifier.error_0 Bool )
(declare-var main@verifier.error.split_0 Bool )
(rule (verifier.error false false false))
(rule (verifier.error false true true))
(rule (verifier.error true false true))
(rule (verifier.error true true true))
(rule (main@entry @unknown_0))
(rule (=> (and (main@entry @unknown_0)
true
(= main@%_0_0 @unknown_0)
(= main@%_2_0 @unknown_0)
(=> main@_bb_0 (and main@_bb_0 main@entry_0))
main@_bb_0
(=> (and main@_bb_0 main@entry_0) (= main@%x.0.i_0 0))
(=> (and main@_bb_0 main@entry_0) (= main@%x.0.i_1 main@%x.0.i_0)))
(main@_bb main@%x.0.i_1 main@%_1_0)))
(rule (let ((a!1 (and (main@_bb main@%x.0.i_0 main@%_1_0)
true
(= main@%_5_0 (< main@%x.0.i_0 main@%_1_0))
(=> main@_bb1_0 (and main@_bb1_0 main@_bb_0))
(=> (and main@_bb1_0 main@_bb_0) main@%_5_0)
(=> main@_bb1_0 (= main@%_7_0 (+ main@%x.0.i_0 1)))
(=> main@_bb_1 (and main@_bb_1 main@_bb1_0))
main@_bb_1
(=> (and main@_bb_1 main@_bb1_0) (= main@%x.0.i_1 main@%_7_0))
(=> (and main@_bb_1 main@_bb1_0)
(= main@%x.0.i_2 main@%x.0.i_1)))))
(=> a!1 (main@_bb main@%x.0.i_2 main@%_1_0))))
(rule (let ((a!1 (and (main@_bb main@%x.0.i_0 main@%_1_0)
true
(= main@%_5_0 (< main@%x.0.i_0 main@%_1_0))
(=> main@_bb2_0 (and main@_bb2_0 main@_bb_0))
(=> (and main@_bb2_0 main@_bb_0) (not main@%_5_0))
(=> main@_bb2_0 (= main@%_9_0 (= main@%x.0.i_0 main@%_1_0)))
(=> main@_bb2_0 (= main@%_10_0 (< main@%_1_0 0)))
(=> main@_bb2_0
(= main@%or.cond.i_0 (or main@%_9_0 main@%_10_0)))
(=> main@_bb2_0 (not main@%or.cond.i_0))
(=> main@_bb2_0 (= main@%_11_0 (xor main@%or.cond.i_0 true)))
(=> main@_bb3_0 (and main@_bb3_0 main@_bb2_0))
(=> main@verifier.error_0
(and main@verifier.error_0 main@_bb3_0))
(=> main@verifier.error.split_0
(and main@verifier.error.split_0 main@verifier.error_0))
main@verifier.error.split_0)))
(=> a!1 main@verifier.error.split)))
(query main@verifier.error.split)