This repository was archived by the owner on Apr 14, 2022. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathexample1.smt2
More file actions
36 lines (29 loc) · 2.05 KB
/
example1.smt2
File metadata and controls
36 lines (29 loc) · 2.05 KB
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
(set-option :produce-unsat-cores true)
; PROGRAM ORDER CONSTRAINTS
(declare-const MAX Int)
(assert (= MAX 8))
(declare-const START_Thread-1@10.0.0.1 Int)
(assert (and (>= START_Thread-1@10.0.0.1 0) (<= START_Thread-1@10.0.0.1 MAX)))
(declare-const W_demos.Example1.counter_Thread-1@10.0.0.1_5@demos.Example1.run.12 Int)
(assert (and (>= W_demos.Example1.counter_Thread-1@10.0.0.1_5@demos.Example1.run.12 0) (<= W_demos.Example1.counter_Thread-1@10.0.0.1_5@demos.Example1.run.12 MAX)))
(declare-const END_Thread-1@10.0.0.1 Int)
(assert (and (>= END_Thread-1@10.0.0.1 0) (<= END_Thread-1@10.0.0.1 MAX)))
(assert (! (< START_Thread-1@10.0.0.1 W_demos.Example1.counter_Thread-1@10.0.0.1_5@demos.Example1.run.12 END_Thread-1@10.0.0.1 ):named PC2))
(declare-const START_main@10.0.0.1 Int)
(assert (and (>= START_main@10.0.0.1 0) (<= START_main@10.0.0.1 MAX)))
(declare-const CREATE_main@10.0.0.1_Thread-1@10.0.0.1 Int)
(assert (and (>= CREATE_main@10.0.0.1_Thread-1@10.0.0.1 0) (<= CREATE_main@10.0.0.1_Thread-1@10.0.0.1 MAX)))
(declare-const W_demos.Example1.counter_main@10.0.0.1_3@demos.Example1.main.7 Int)
(assert (and (>= W_demos.Example1.counter_main@10.0.0.1_3@demos.Example1.main.7 0) (<= W_demos.Example1.counter_main@10.0.0.1_3@demos.Example1.main.7 MAX)))
(declare-const W_demos.Example1.counter_main@10.0.0.1_4@demos.Example1.main.8 Int)
(assert (and (>= W_demos.Example1.counter_main@10.0.0.1_4@demos.Example1.main.8 0) (<= W_demos.Example1.counter_main@10.0.0.1_4@demos.Example1.main.8 MAX)))
(declare-const END_main@10.0.0.1 Int)
(assert (and (>= END_main@10.0.0.1 0) (<= END_main@10.0.0.1 MAX)))
(assert (! (< START_main@10.0.0.1 CREATE_main@10.0.0.1_Thread-1@10.0.0.1 W_demos.Example1.counter_main@10.0.0.1_3@demos.Example1.main.7 W_demos.Example1.counter_main@10.0.0.1_4@demos.Example1.main.8 END_main@10.0.0.1 ):named PC3))
; FORK-START CONSTRAINTS
(assert (! (< CREATE_main@10.0.0.1_Thread-1@10.0.0.1 START_Thread-1@10.0.0.1):named FS4))
; JOIN-END CONSTRAINTS
; WAIT-NOTIFY CONSTRAINTS
; LOCKING CONSTRAINTS
; SEND-RECEIVE CONSTRAINTS
; RECEIVE-HANDLER LINKAGE CONSTRAINTS