mgudemann / iimc Goto Github PK

I have seen there are some special tatics in iimc, the README indicated that "Combinations of proof engines are supported by special tactics: fork, join, begin, end. While these tactics are exposed by the interface, only a few of the syntactically meaningful combinations are supported and they are not meant for general use."

However, I have seen any details instructions to use this in README, could you give me a simple example to apply it? Thanks

iimc examples/ctl/palu.aig --ctl examples/ctl/palu.ctl --print_cex --iictl_verbosity 3 --pi 0
will give you a segment fault. Tried the --print_cex flag on numerous aigs and ctls all end up with the same issue.

currently, selecting MiniSAT as ic3 back-end will not work on ic3r, for which zchaff is always used

Running IIMC on the AAG file below (without any parameters) sometimes yields "1" as result, but also sometimes yields:

iimc: src/mc/ProofAttachment.h:85: void ProofAttachment::setConclusion(int): Assertion `_safe == conclusion' failed.

Running "valgrind --tool=memcheck ./imc inputFile" always leads to the assumption violation. The AAG file below is accepted without complaints by "aigbmc" from the AIGER tool set

aag 171 18 36 0 111 0 0 1
2
4
6
8
10
22
24
26
28
30
32
34
36
38
40
42
44
46
48 2
50 4
52 6
54 8
56 10
58 12
60 14
62 18
64 20
66 22
68 24
70 26
72 28
74 30
76 32
78 34
80 36
82 38
84 40
86 42
88 44
90 46
92 264
94 1
318 2
320 4
322 6
324 8
326 10
328 1
330 0
332 1
334 1
336 1
338 342
340 343
5
278
284
298
302
304
96 11 6
98 96 5
100 98 3
102 35 15
104 42 30
106 43 31
108 107 105
110 109 43
112 108 42
114 113 111
116 115 33
118 117 103
120 118 37
122 42 8
124 123 13
126 38 14
128 127 41
130 128 124
132 131 40
134 132 45
136 134 120
138 136 100
140 104 23
142 140 25
144 143 103
146 144 27
148 40 15
150 148 29
152 150 146
154 153 138
156 155 47
158 156 95
160 146 70
162 147 71
164 163 161
166 142 68
168 143 69
170 169 167
172 170 164
174 66 19
176 67 18
178 177 175
180 178 172
182 150 72
184 151 73
186 185 183
188 186 180
190 120 80
192 121 81
194 193 191
196 194 188
198 116 76
200 117 77
202 201 199
204 202 196
206 74 21
208 75 20
210 209 207
212 210 204
214 102 78
216 103 79
218 217 215
220 218 212
222 134 88
224 135 89
226 225 223
228 226 220
230 82 7
232 83 6
234 233 231
236 234 228
238 84 9
240 85 8
242 241 239
244 242 236
246 86 11
248 87 10
250 249 247
252 250 244
254 253 91
256 90 47
258 257 255
260 258 92
262 261 94
264 263 159
266 79 61
268 86 74
270 268 67
272 270 69
274 273 267
276 274 70
278 277 92
280 84 61
282 280 72
284 283 92
286 87 75
288 287 269
290 289 87
292 288 86
294 293 291
296 295 76
298 297 92
300 78 61
302 301 92
304 92 91
342 341 339
12 1 1
14 0 1
16 1 1
18 1 1
20 1 1
i0 AIGER_NEXT_a
i1 AIGER_NEXT_b
i2 AIGER_NEXT_c
i3 AIGER_NEXT_d
i4 AIGER_NEXT_e
i5 AIGER_NEXT_LTL_1_SPECF_18
i6 AIGER_NEXT_LTL_1_SPECF_17
i7 AIGER_NEXT_LTL_1_SPECF_15
i8 AIGER_NEXT_LTL_1_SPECF_13
i9 AIGER_NEXT_LTL_1_SPECF_11
i10 AIGER_NEXT_LTL_1_SPECF_10
i11 AIGER_NEXT_LTL_1_SPECF_8
i12 AIGER_NEXT_LTL_1_SPECF_6
i13 AIGER_NEXT_LTL_1_SPECF_4
i14 AIGER_NEXT_LTL_1_SPECF_3
i15 AIGER_NEXT_LTL_1_SPECF_2
i16 AIGER_NEXT_LTL_1_SPECF_1
i17 AIGER_NEXT_IGNORE_LTL_1
l0 a
l1 b
l2 c
l3 d
l4 e
l5 u
l6 v
l7 x
l8 y
l9 LTL_1_SPECF_18
l10 LTL_1_SPECF_17
l11 LTL_1_SPECF_15
l12 LTL_1_SPECF_13
l13 LTL_1_SPECF_11
l14 LTL_1_SPECF_10
l15 LTL_1_SPECF_8
l16 LTL_1_SPECF_6
l17 LTL_1_SPECF_4
l18 LTL_1_SPECF_3
l19 LTL_1_SPECF_2
l20 LTL_1_SPECF_1
l21 IGNORE_LTL_1
l22 AIGER_VALID
l23 AIGER_INITIALIZED
j0 AIGER_JUST_0