QualifiedCProgramming/run-example-linux.sh at main · QinxiangCao/QualifiedCProgramming · GitHub

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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
#!/bin/bash
set -e

cleanup_sacgen_tmp() {
  find . -type f -name '*.sacgen.tmp' -delete
}
trap cleanup_sacgen_tmp EXIT

linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/simple_arith/gcd_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/simple_arith/gcd_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/simple_arith/gcd_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human.simple_arith -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/simple_arith/gcd.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/simple_arith/gcd_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/simple_arith/gcd_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/simple_arith/gcd_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM.simple_arith -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/simple_arith/gcd.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/simple_arith/exgcd_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/simple_arith/exgcd_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/simple_arith/exgcd_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human.simple_arith -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/simple_arith/exgcd.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/simple_arith/exgcd_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/simple_arith/exgcd_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/simple_arith/exgcd_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM.simple_arith -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/simple_arith/exgcd.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/simple_arith/abs_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/simple_arith/abs_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/simple_arith/abs_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human.simple_arith -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/simple_arith/abs.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/simple_arith/abs_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/simple_arith/abs_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/simple_arith/abs_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM.simple_arith -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/simple_arith/abs.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/simple_arith/add_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/simple_arith/add_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/simple_arith/add_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human.simple_arith -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/simple_arith/add.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/simple_arith/add_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/simple_arith/add_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/simple_arith/add_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM.simple_arith -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/simple_arith/add.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/simple_arith/max3_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/simple_arith/max3_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/simple_arith/max3_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human.simple_arith -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/simple_arith/max3.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/simple_arith/max3_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/simple_arith/max3_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/simple_arith/max3_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM.simple_arith -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/simple_arith/max3.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/simple_arith/div_test_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/simple_arith/div_test_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/simple_arith/div_test_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human.simple_arith -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/simple_arith/div_test.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/simple_arith/div_test_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/simple_arith/div_test_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/simple_arith/div_test_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM.simple_arith -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/simple_arith/div_test.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/simple_arith/Always_pos_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/simple_arith/Always_pos_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/simple_arith/Always_pos_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human.simple_arith -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/simple_arith/Always_pos.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/simple_arith/Always_pos_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/simple_arith/Always_pos_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/simple_arith/Always_pos_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM.simple_arith -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/simple_arith/Always_pos.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/simple_arith/delta_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/simple_arith/delta_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/simple_arith/delta_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM.simple_arith -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/simple_arith/delta.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/simple_arith/test_prime_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/simple_arith/test_prime_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/simple_arith/test_prime_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM.simple_arith -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/simple_arith/test_prime.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/poly_sll_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/poly_sll_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/poly_sll_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/poly_sll.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/poly_sll_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/poly_sll_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/poly_sll_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/poly_sll.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/bubble_sort_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/bubble_sort_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/bubble_sort_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/bubble_sort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/sll_auto_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/sll_auto_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/sll_auto_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sll_auto.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/sll_auto_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/sll_auto_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/sll_auto_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sll_auto.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/sll_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/sll_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/sll_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sll.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/sll_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/sll_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/sll_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sll.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/dll_auto_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/dll_auto_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/dll_auto_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/dll_auto.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/dll_auto_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/dll_auto_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/dll_auto_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/dll_auto.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/sll_insert_sort_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/sll_insert_sort_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/sll_insert_sort_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sll_insert_sort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/sll_insert_sort_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/sll_insert_sort_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/sll_insert_sort_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sll_insert_sort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/dll_queue_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/dll_queue_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/dll_queue_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/dll_queue.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/dll_queue_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/dll_queue_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/dll_queue_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/dll_queue.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/functional_queue_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/functional_queue_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/functional_queue_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/functional_queue.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/functional_queue_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/functional_queue_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/functional_queue_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/functional_queue.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/sll_queue_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/sll_queue_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/sll_queue_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sll_queue.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/sll_queue_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/sll_queue_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/sll_queue_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sll_queue.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/sum_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/sum_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/sum_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sum.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/sum_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/sum_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/sum_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sum.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/swap_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/swap_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/swap_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/swap.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/swap_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/swap_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/swap_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/swap.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/bst_insert_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/bst_insert_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/bst_insert_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/bst_insert.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/bst_insert_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/bst_insert_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/bst_insert_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/bst_insert.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/bst_fp_insert_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/bst_fp_insert_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/bst_fp_insert_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/bst_fp_insert.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/bst_fp_insert_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/bst_fp_insert_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/bst_fp_insert_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/bst_fp_insert.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/bst_fp_delete_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/bst_fp_delete_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/bst_fp_delete_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/bst_fp_delete.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/bst_fp_delete_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/bst_fp_delete_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/bst_fp_delete_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/bst_fp_delete.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/bst_insert_rec_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/bst_insert_rec_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/bst_insert_rec_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/bst_insert_rec.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/bst_insert_rec_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/bst_insert_rec_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/bst_insert_rec_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/bst_insert_rec.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/bst_delete_rec_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/bst_delete_rec_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/bst_delete_rec_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/bst_delete_rec.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/bst_delete_rec_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/bst_delete_rec_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/bst_delete_rec_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/bst_delete_rec.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/bst_delete_rec2_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/bst_delete_rec2_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/bst_delete_rec2_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/bst_delete_rec2.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/bst_delete_rec2_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/bst_delete_rec2_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/bst_delete_rec2_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/bst_delete_rec2.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/eval_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/eval_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/eval_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/eval.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/eval_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/eval_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/eval_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/eval.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/typeinfer/typeinfer_goal.v --proof-auto-file=Rocq/examples/Applications_human/typeinfer/typeinfer_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/typeinfer/typeinfer_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.typeinfer --input-file=QCP_examples/Applications_human/typeinfer/typeinfer.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/fme/fme_goal.v --proof-auto-file=Rocq/examples/Applications_human/fme/fme_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/fme/fme_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.fme --input-file=QCP_examples/Applications_human/fme/fme.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/common.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/common.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/poly_sll.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/poly_sll.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sll_shape.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sll_shape.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/dll_shape.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/dll_shape.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sll.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sll.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/dll_queue.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/dll_queue.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/functional_queue.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/functional_queue.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sll_queue.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sll_queue.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/int_array.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/int_array.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/uint_array.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/uint_array.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/bst.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/bst.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/bst_fp.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/bst_fp.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/eval.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/eval.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/typeinfer/ --coq-logic-path=SimpleC.EE.Applications_human.typeinfer -IQCP_examples/QCP_demos_human/ --input-file=QCP_examples/Applications_human/typeinfer/typeinfer.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/fme/ --coq-logic-path=SimpleC.EE.Applications_human.fme -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ --input-file=QCP_examples/Applications_human/fme/fme.strategies --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/avl_insert_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/avl_insert_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/avl_insert_proof_manual.v -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human -IQCP_examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/avl_insert.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/avl_insert_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/avl_insert_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/avl_insert_proof_manual.v -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM -IQCP_examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/avl_insert.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/avl.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/avl.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/ --coq-logic-path=SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ --input-file=QCP_examples/Applications_human/los_sortlink.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/char_array.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/char_array.strategies --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/Get_Set_Value_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/Get_Set_Value_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/Get_Set_Value_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/Get_Set_Value.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/GetSortLinkNextExpireTime_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/GetSortLinkNextExpireTime_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/GetSortLinkNextExpireTime_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/GetSortLinkNextExpireTime.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/List_Add_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/List_Add_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/List_Add_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/List_Add.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/LOS_ListDelete_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/LOS_ListDelete_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/LOS_ListDelete_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/LOS_ListDelete.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/LOS_ListDelInit_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/LOS_ListDelInit_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/LOS_ListDelInit_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/LOS_ListDelInit.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/LOS_ListEmpty_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/LOS_ListEmpty_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/LOS_ListEmpty_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/LOS_ListEmpty.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/LOS_ListInit_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/LOS_ListInit_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/LOS_ListInit_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/LOS_ListInit.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsAdd2SortLink_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsAdd2SortLink_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsAdd2SortLink_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsAdd2SortLink.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsDeleteNodeSortLink_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsDeleteNodeSortLink_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsDeleteNodeSortLink_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsDeleteNodeSortLink.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsDeleteSortLink_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsDeleteSortLink_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsDeleteSortLink_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsDeleteSortLink.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsGetNextExpireTime_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsGetNextExpireTime_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsGetNextExpireTime_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsGetNextExpireTime.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsGetSortLinkAttribute_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsGetSortLinkAttribute_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsGetSortLinkAttribute_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsGetSortLinkAttribute.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkGetNextExpireTime_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkGetNextExpireTime_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkGetNextExpireTime_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsSortLinkGetNextExpireTime.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkGetRemainTime_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkGetRemainTime_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkGetRemainTime_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsSortLinkGetRemainTime.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkGetTargetExpireTime_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkGetTargetExpireTime_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkGetTargetExpireTime_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsSortLinkGetTargetExpireTime.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkInit_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkInit_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkInit_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsSortLinkInit.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkResponseTimeConvertFreq_goal.v --proof-auto-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkResponseTimeConvertFreq_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/LiteOS/OsSortLinkResponseTimeConvertFreq_proof_manual.v -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.LiteOS --input-file=QCP_examples/Applications_human/LiteOS/OsSortLinkResponseTimeConvertFreq.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/minigmp/gmp_goal.v --proof-auto-file=Rocq/examples/Applications_human/minigmp/gmp_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/minigmp/gmp_proof_manual.v -slp QCP_examples/Applications_human/minigmp/ SimpleC.EE.Applications_human.minigmp -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.minigmp --input-file=QCP_examples/Applications_human/minigmp/gmp.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/minigmp_sumlib/gmp_goal.v --proof-auto-file=Rocq/examples/Applications_human/minigmp_sumlib/gmp_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/minigmp_sumlib/gmp_proof_manual.v -IQCP_examples/Applications_human/minigmp_sumlib/ -slp QCP_examples/Applications_human/minigmp/ SimpleC.EE.Applications_human.minigmp -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.minigmp_sumlib --input-file=QCP_examples/Applications_human/minigmp_sumlib/gmp.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/cnf_trans/cnf_trans_goal.v --proof-auto-file=Rocq/examples/Applications_human/cnf_trans/cnf_trans_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/cnf_trans/cnf_trans_proof_manual.v -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.cnf_trans --input-file=QCP_examples/Applications_human/cnf_trans/cnf_trans.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/alpha_equiv/alpha_equiv_goal.v --proof-auto-file=Rocq/examples/Applications_human/alpha_equiv/alpha_equiv_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/alpha_equiv/alpha_equiv_proof_manual.v -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.alpha_equiv --input-file=QCP_examples/Applications_human/alpha_equiv/alpha_equiv.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/alpha_equiv/subst_goal.v --proof-auto-file=Rocq/examples/Applications_human/alpha_equiv/subst_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/alpha_equiv/subst_proof_manual.v -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.alpha_equiv --input-file=QCP_examples/Applications_human/alpha_equiv/subst.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/alpha_equiv/thm_apply_goal.v --proof-auto-file=Rocq/examples/Applications_human/alpha_equiv/thm_apply_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/alpha_equiv/thm_apply_proof_manual.v -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_human/ -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --coq-logic-path=SimpleC.EE.Applications_human.alpha_equiv --input-file=QCP_examples/Applications_human/alpha_equiv/thm_apply.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/array_auto_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/array_auto_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/array_auto_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/array_auto.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/array_auto_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/array_auto_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/array_auto_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/array_auto.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/chars_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/chars_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/chars_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/chars.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/chars_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/chars_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/chars_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/chars.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/majority_element/majority_element_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/majority_element/majority_element_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/majority_element/majority_element_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.majority_element -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/majority_element/majority_element.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/safeexec.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/safeexec.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/array_shape.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/array_shape.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/undef_uint_array.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/undef_uint_array.strategies --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/int_array_merge_rel_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/int_array_merge_rel_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/int_array_merge_rel_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/int_array_merge_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/int_array_merge_rel_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/int_array_merge_rel_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/int_array_merge_rel_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/int_array_merge_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/branch_destruct_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/branch_destruct_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/branch_destruct_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ --input-file=QCP_examples/QCP_demos_tutorial/branch_destruct.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/branch_join_private_condition_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/branch_join_private_condition_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/branch_join_private_condition_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ --input-file=QCP_examples/QCP_demos_tutorial/branch_join_private_condition.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/given_mark_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/given_mark_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/given_mark_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ --input-file=QCP_examples/QCP_demos_tutorial/given_mark.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/multiinv_examples_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/multiinv_examples_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/multiinv_examples_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ --input-file=QCP_examples/QCP_demos_tutorial/multiinv_examples.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/sll_merge_rel_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/sll_merge_rel_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/sll_merge_rel_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sll_merge_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/sll_merge_rel_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/sll_merge_rel_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/sll_merge_rel_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sll_merge_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/sll_split_while_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/sll_split_while_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/sll_split_while_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/sll_split_while.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/sll_split_while_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/sll_split_while_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/sll_split_while_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/sll_split_while.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_human/kmp_rel_goal.v --proof-auto-file=Rocq/examples/QCP_demos_human/kmp_rel_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_human/kmp_rel_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/kmp_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/kmp_rel_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/kmp_rel_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/kmp_rel_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/kmp_rel.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_human/ --coq-logic-path=SimpleC.EE.QCP_demos_human --input-file=QCP_examples/QCP_demos_human/safeexecE.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/safeexecE.strategies --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/insertion_sort/insertion_sort_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/insertion_sort/insertion_sort_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/insertion_sort/insertion_sort_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.insertion_sort -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/insertion_sort/insertion_sort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/selection_sort/selection_sort_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/selection_sort/selection_sort_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/selection_sort/selection_sort_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.selection_sort -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/selection_sort/selection_sort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/annoying_math_homework/annoying_math_homework_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/annoying_math_homework/annoying_math_homework_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/annoying_math_homework/annoying_math_homework_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.annoying_math_homework -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/annoying_math_homework/annoying_math_homework.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/stock_trading/stock_trading_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/stock_trading/stock_trading_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/stock_trading/stock_trading_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.stock_trading -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/stock_trading/stock_trading.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/bubble_sort/bubble_sort_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/bubble_sort/bubble_sort_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/bubble_sort/bubble_sort_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.bubble_sort -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/bubble_sort/bubble_sort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/catalan_numbers/catalan_numbers_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/catalan_numbers/catalan_numbers_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/catalan_numbers/catalan_numbers_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.catalan_numbers -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/catalan_numbers/catalan_numbers.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/choir_singing/choir_singing_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/choir_singing/choir_singing_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/choir_singing/choir_singing_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.choir_singing -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/choir_singing/choir_singing.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/choosing_inns/choosing_inns_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/choosing_inns/choosing_inns_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/choosing_inns/choosing_inns_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.choosing_inns -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/choosing_inns/choosing_inns.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/DFS/DFS_adjacency_list_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/DFS/DFS_adjacency_list_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/DFS/DFS_adjacency_list_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.DFS -IQCP_examples/LLM_bench/Algorithms/DFS/ -slp QCP_examples/LLM_bench/Algorithms/DFS/ SimpleC.EE.LLM_bench.Algorithms.DFS -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/DFS/DFS_adjacency_list.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/DFS/DFS_adjacency_matrix_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/DFS/DFS_adjacency_matrix_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/DFS/DFS_adjacency_matrix_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.DFS -IQCP_examples/LLM_bench/Algorithms/DFS/ -slp QCP_examples/LLM_bench/Algorithms/DFS/ SimpleC.EE.LLM_bench.Algorithms.DFS -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/DFS/DFS_adjacency_matrix.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/DFS/DFS_adjacency_matrix_2Darray_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/DFS/DFS_adjacency_matrix_2Darray_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/DFS/DFS_adjacency_matrix_2Darray_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.DFS -IQCP_examples/LLM_bench/Algorithms/DFS/ -slp QCP_examples/LLM_bench/Algorithms/DFS/ SimpleC.EE.LLM_bench.Algorithms.DFS -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/DFS/DFS_adjacency_matrix_2Darray.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/Floyd/Floyd_adjacency_matrix_2Darray_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/Floyd/Floyd_adjacency_matrix_2Darray_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/Floyd/Floyd_adjacency_matrix_2Darray_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.Floyd -IQCP_examples/LLM_bench/Algorithms/Floyd/ -slp QCP_examples/LLM_bench/Algorithms/Floyd/ SimpleC.EE.LLM_bench.Algorithms.Floyd -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/Floyd/Floyd_adjacency_matrix_2Darray.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/Dijkstra/Dijkstra_linked_forward_star_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/Dijkstra/Dijkstra_linked_forward_star_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/Dijkstra/Dijkstra_linked_forward_star_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.Dijkstra -IQCP_examples/LLM_bench/Algorithms/Dijkstra/ -slp QCP_examples/LLM_bench/Algorithms/Dijkstra/ SimpleC.EE.LLM_bench.Algorithms.Dijkstra -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/Dijkstra/Dijkstra_linked_forward_star.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/discretize/discretize_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/discretize/discretize_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/discretize/discretize_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.discretize -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/discretize/discretize.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/edit_strings/edit_strings_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/edit_strings/edit_strings_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/edit_strings/edit_strings_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.edit_strings -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/edit_strings/edit_strings.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/energy_necklace/energy_necklace_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/energy_necklace/energy_necklace_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/energy_necklace/energy_necklace_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.energy_necklace -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/energy_necklace/energy_necklace.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/kings_game/kings_game_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/kings_game/kings_game_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/kings_game/kings_game_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.kings_game -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/kings_game/kings_game.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/longest_increasing_subsequence/longest_increasing_subsequence_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/longest_increasing_subsequence/longest_increasing_subsequence_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/longest_increasing_subsequence/longest_increasing_subsequence_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.longest_increasing_subsequence -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/longest_increasing_subsequence/longest_increasing_subsequence.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Data_structures/priority_queue/priority_queue_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Data_structures/priority_queue/priority_queue_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Data_structures/priority_queue/priority_queue_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Data_structures.priority_queue -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Data_structures/priority_queue/priority_queue.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/coin_change/coin_change_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/coin_change/coin_change_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/coin_change/coin_change_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.coin_change -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/coin_change/coin_change.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/concatenating_numbers/concatenating_numbers_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/concatenating_numbers/concatenating_numbers_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/concatenating_numbers/concatenating_numbers_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.concatenating_numbers -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/concatenating_numbers/concatenating_numbers.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/concatenating_numbers_dp/concatenating_numbers_dp_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/concatenating_numbers_dp/concatenating_numbers_dp_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/concatenating_numbers_dp/concatenating_numbers_dp_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.concatenating_numbers_dp -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/concatenating_numbers_dp/concatenating_numbers_dp.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/house_robber/house_robber_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/house_robber/house_robber_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/house_robber/house_robber_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.house_robber -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/house_robber/house_robber.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/longest_nondecreasing_subsequence/longest_nondecreasing_subsequence_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/longest_nondecreasing_subsequence/longest_nondecreasing_subsequence_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/longest_nondecreasing_subsequence/longest_nondecreasing_subsequence_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.longest_nondecreasing_subsequence -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/longest_nondecreasing_subsequence/longest_nondecreasing_subsequence.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/maximum_subarray/maximum_subarray_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/maximum_subarray/maximum_subarray_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/maximum_subarray/maximum_subarray_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.maximum_subarray -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/maximum_subarray/maximum_subarray.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/merging_stones/merging_stones_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/merging_stones/merging_stones_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/merging_stones/merging_stones_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.merging_stones -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/merging_stones/merging_stones.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/multiple_knapsack/multiple_knapsack_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/multiple_knapsack/multiple_knapsack_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/multiple_knapsack/multiple_knapsack_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.multiple_knapsack -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/multiple_knapsack/multiple_knapsack.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/paint_house_ii/paint_house_ii_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/paint_house_ii/paint_house_ii_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/paint_house_ii/paint_house_ii_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.paint_house_ii -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/paint_house_ii/paint_house_ii.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_fill_index/quicksort_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_fill_index/quicksort_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_fill_index/quicksort_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.quicksort_hoare_fill_index -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/quicksort_hoare_fill_index/quicksort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_fill_index2/quicksort_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_fill_index2/quicksort_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_fill_index2/quicksort_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.quicksort_hoare_fill_index2 -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/quicksort_hoare_fill_index2/quicksort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_swap_index/quicksort_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_swap_index/quicksort_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_swap_index/quicksort_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.quicksort_hoare_swap_index -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/quicksort_hoare_swap_index/quicksort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_swap_index2/quicksort_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_swap_index2/quicksort_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/quicksort_hoare_swap_index2/quicksort_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.quicksort_hoare_swap_index2 -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/quicksort_hoare_swap_index2/quicksort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/quicksort_lomuto_index/quicksort_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/quicksort_lomuto_index/quicksort_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/quicksort_lomuto_index/quicksort_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.quicksort_lomuto_index -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/quicksort_lomuto_index/quicksort.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/rmq/rmq_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/rmq/rmq_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/rmq/rmq_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.rmq -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/rmq/rmq.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/max_sum_increasing_sequence/max_sum_increasing_sequence_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/max_sum_increasing_sequence/max_sum_increasing_sequence_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/max_sum_increasing_sequence/max_sum_increasing_sequence_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.max_sum_increasing_sequence -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/max_sum_increasing_sequence/max_sum_increasing_sequence.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/sieve_of_eratosthenes/sieve_of_eratosthenes_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/sieve_of_eratosthenes/sieve_of_eratosthenes_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/sieve_of_eratosthenes/sieve_of_eratosthenes_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.sieve_of_eratosthenes -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/sieve_of_eratosthenes/sieve_of_eratosthenes.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/sieve_of_euler/sieve_of_euler_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/sieve_of_euler/sieve_of_euler_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/sieve_of_euler/sieve_of_euler_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.sieve_of_euler -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/sieve_of_euler/sieve_of_euler.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/sliding_window_maximum/sliding_window_maximum_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/sliding_window_maximum/sliding_window_maximum_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/sliding_window_maximum/sliding_window_maximum_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.sliding_window_maximum -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/sliding_window_maximum/sliding_window_maximum.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/sort_point/sort_point_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/sort_point/sort_point_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/sort_point/sort_point_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.sort_point -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/sort_point/sort_point.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/split_array_largest_sum/split_array_largest_sum_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/split_array_largest_sum/split_array_largest_sum_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/split_array_largest_sum/split_array_largest_sum_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.split_array_largest_sum -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/split_array_largest_sum/split_array_largest_sum.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/super_piano/super_piano_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/super_piano/super_piano_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/super_piano/super_piano_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.super_piano -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/super_piano/super_piano.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/zero_one_knapsack/zero_one_knapsack_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/zero_one_knapsack/zero_one_knapsack_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/zero_one_knapsack/zero_one_knapsack_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.zero_one_knapsack -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/zero_one_knapsack/zero_one_knapsack.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/stdlib/ --coq-logic-path=SimpleC.StdLib --input-file=QCP_examples/stdlib/string.strategies -IQCP_examples/stdlib/ -slp QCP_examples/stdlib/ SimpleC.StdLib -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/string/memchr_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/string/memchr_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/string/memchr_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.string -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/stdlib/ -slp QCP_examples/stdlib/ SimpleC.StdLib -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/string/memchr.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/string/memory_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/string/memory_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/string/memory_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.string -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/stdlib/ -slp QCP_examples/stdlib/ SimpleC.StdLib -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/string/memory.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/string/search_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/string/search_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/string/search_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.string -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/stdlib/ -slp QCP_examples/stdlib/ SimpleC.StdLib -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/string/search.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/string/strcat_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/string/strcat_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/string/strcat_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.string -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/stdlib/ -slp QCP_examples/stdlib/ SimpleC.StdLib -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/string/strcat.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/string/strcmp_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/string/strcmp_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/string/strcmp_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.string -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/stdlib/ -slp QCP_examples/stdlib/ SimpleC.StdLib -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/string/strcmp.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/string/strcpy_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/string/strcpy_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/string/strcpy_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.string -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/stdlib/ -slp QCP_examples/stdlib/ SimpleC.StdLib -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/string/strcpy.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/string/strlen_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/string/strlen_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/string/strlen_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.string -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/stdlib/ -slp QCP_examples/stdlib/ SimpleC.StdLib -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/string/strlen.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/list_tail_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/list_tail_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/list_tail_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/list_tail_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/list_append_raw_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/list_append_raw_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/list_append_raw_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/list_append_raw_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_app_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_app_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_app_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_app_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_copy_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_copy_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_copy_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_copy_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_free_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_free_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_free_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_free_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_back_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_back_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_back_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_back_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_back_2_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_back_2_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_back_2_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_back_2_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_twice_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_twice_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_twice_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_iter_twice_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_merge_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_merge_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_merge_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_merge_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_append_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_append_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_append_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_append_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_merge_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_merge_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_merge_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_merge_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_rev_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_rev_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_rev_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_multi_rev_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_append_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_append_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_append_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_append_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_append_twice_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_append_twice_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_append_twice_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_append_twice_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_rel_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_rel_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_rel_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Engineering.glibc_slist.glibc_slist_rel -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/ -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Engineering/glibc_slist/glibc_slist_rel/glibc_slist_rev_rel.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/array_cases_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/array_cases_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/array_cases_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/array_cases.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/union_find_err_rel_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/union_find_err_rel_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/union_find_err_rel_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/union_find_err_rel.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/array2.strategies -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/int_ptr_array2.strategies -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_LLM/ --coq-logic-path=SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/ptr_array2.strategies -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/two_d_int_array_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/two_d_int_array_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/two_d_int_array_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/2DIntArray.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/two_d_int_ptr_array_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/two_d_int_ptr_array_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/two_d_int_ptr_array_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/2DIntPtrArray.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/two_d_char_ptr_array_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/two_d_char_ptr_array_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/two_d_char_ptr_array_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/2DCharPtrArray.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/three_d_graph_field_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/three_d_graph_field_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/three_d_graph_field_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/3DGraphField.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_LLM/three_d_graph_field_one_read_goal.v --proof-auto-file=Rocq/examples/QCP_demos_LLM/three_d_graph_field_one_read_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_LLM/three_d_graph_field_one_read_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_LLM -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/QCP_demos_LLM/3DGraphFieldOneRead.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/manacher/manacher_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/manacher/manacher_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/manacher/manacher_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.manacher -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/stdlib/ -slp QCP_examples/stdlib/ SimpleC.StdLib -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/manacher/manacher.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/minigmp/ --coq-logic-path=SimpleC.EE.Applications_human.minigmp -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ --input-file=QCP_examples/Applications_human/minigmp/gmp.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/mergeablelist/ --coq-logic-path=SimpleC.EE.Applications_human.mergeablelist -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/Applications_human/mergeablelist/ SimpleC.EE.Applications_human.mergeablelist --input-file=QCP_examples/Applications_human/mergeablelist/sll_project.strategies --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/mergeablelist/sll_project_goal.v --proof-auto-file=Rocq/examples/Applications_human/mergeablelist/sll_project_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/mergeablelist/sll_project_proof_manual.v -IQCP_examples/Applications_human/ -IQCP_examples/QCP_demos_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -slp QCP_examples/QCP_demos_human/ SimpleC.EE.QCP_demos_human -slp QCP_examples/Applications_human/mergeablelist/ SimpleC.EE.Applications_human.mergeablelist --coq-logic-path=SimpleC.EE.Applications_human.mergeablelist --input-file=QCP_examples/Applications_human/mergeablelist/sll_project_lib.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/swap_simple1_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/swap_simple1_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/swap_simple1_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/swap_simple1.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_tutorial/ --coq-logic-path=SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/swap_simple2.strategies -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/swap_simple2_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/swap_simple2_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/swap_simple2_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/swap_simple2.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_tutorial/ --coq-logic-path=SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/swap_simple3.strategies -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/swap_simple3_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/swap_simple3_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/swap_simple3_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/swap_simple3.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_tutorial/ --coq-logic-path=SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/swap_simple4.strategies -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/swap_simple4_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/swap_simple4_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/swap_simple4_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/swap_simple4.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_tutorial/ --coq-logic-path=SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/swap_simple5.strategies -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/swap_simple5_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/swap_simple5_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/swap_simple5_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/swap_simple5.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/float_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/float_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/float_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/float.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/QCP_demos_tutorial/ --coq-logic-path=SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/pos_int_pair.strategies -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/QCP_demos_tutorial/pos_int_pair_goal.v --proof-auto-file=Rocq/examples/QCP_demos_tutorial/pos_int_pair_proof_auto.v --proof-manual-file=Rocq/examples/QCP_demos_tutorial/pos_int_pair_proof_manual.v --coq-logic-path=SimpleC.EE.QCP_demos_tutorial -IQCP_examples/QCP_demos_tutorial/ -slp QCP_examples/QCP_demos_tutorial/ SimpleC.EE.QCP_demos_tutorial --input-file=QCP_examples/QCP_demos_tutorial/pos_int_pair.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/convex_hull/ --coq-logic-path=SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/convex_hull/ -slp QCP_examples/Applications_human/convex_hull/ SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/Applications_human/convex_hull/point_array.strategies --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/convex_hull/ --coq-logic-path=SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/convex_hull/ -slp QCP_examples/Applications_human/convex_hull/ SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/Applications_human/convex_hull/safeexec.strategies --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/convex_hull/graham_scan_goal.v --proof-auto-file=Rocq/examples/Applications_human/convex_hull/graham_scan_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/convex_hull/graham_scan_proof_manual.v --coq-logic-path=SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/convex_hull/ -slp QCP_examples/Applications_human/convex_hull/ SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/Applications_human/convex_hull/graham_scan.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/convex_hull/graham_scan_dedup_goal.v --proof-auto-file=Rocq/examples/Applications_human/convex_hull/graham_scan_dedup_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/convex_hull/graham_scan_dedup_proof_manual.v --coq-logic-path=SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/convex_hull/ -slp QCP_examples/Applications_human/convex_hull/ SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/Applications_human/convex_hull/graham_scan_dedup.c --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/convex_hull/andrew_monotone_chain_goal.v --proof-auto-file=Rocq/examples/Applications_human/convex_hull/andrew_monotone_chain_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/convex_hull/andrew_monotone_chain_proof_manual.v --coq-logic-path=SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/convex_hull/ -slp QCP_examples/Applications_human/convex_hull/ SimpleC.EE.Applications_human.convex_hull -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/Applications_human/convex_hull/andrew_monotone_chain.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/CDCL/ --coq-logic-path=SimpleC.EE.Applications_human.CDCL -IQCP_examples/Applications_human/CDCL/ -slp QCP_examples/Applications_human/CDCL/ SimpleC.EE.Applications_human.CDCL -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/Applications_human/CDCL/CDCL_qcp.strategies --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/Applications_human/CDCL/CDCL_qcp_goal.v --proof-auto-file=Rocq/examples/Applications_human/CDCL/CDCL_qcp_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/CDCL/CDCL_qcp_proof_manual.v --coq-logic-path=SimpleC.EE.Applications_human.CDCL -IQCP_examples/Applications_human/CDCL/ -slp QCP_examples/Applications_human/CDCL/ SimpleC.EE.Applications_human.CDCL -IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/Applications_human/CDCL/CDCL_qcp.c --no-exec-info;
linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/LLM_bench/Algorithms/convex_hull_float/ --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.convex_hull_float -IQCP_examples/LLM_bench/Algorithms/convex_hull_float/ -slp QCP_examples/LLM_bench/Algorithms/convex_hull_float/ SimpleC.EE.LLM_bench.Algorithms.convex_hull_float -IQCP_examples/LLM_bench/ -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/convex_hull_float/pointf_array.strategies --no-exec-info;
linux-binary/symexec --goal-file=Rocq/examples/LLM_bench/Algorithms/convex_hull_float/convex_hull_float_goal.v --proof-auto-file=Rocq/examples/LLM_bench/Algorithms/convex_hull_float/convex_hull_float_proof_auto.v --proof-manual-file=Rocq/examples/LLM_bench/Algorithms/convex_hull_float/convex_hull_float_proof_manual.v --coq-logic-path=SimpleC.EE.LLM_bench.Algorithms.convex_hull_float -IQCP_examples/LLM_bench/Algorithms/convex_hull_float/ -slp QCP_examples/LLM_bench/Algorithms/convex_hull_float/ SimpleC.EE.LLM_bench.Algorithms.convex_hull_float -IQCP_examples/LLM_bench/ -slp QCP_examples/LLM_bench/ SimpleC.EE.LLM_bench -IQCP_examples/QCP_demos_LLM/ -slp QCP_examples/QCP_demos_LLM/ SimpleC.EE.QCP_demos_LLM --input-file=QCP_examples/LLM_bench/Algorithms/convex_hull_float/convex_hull_float.c --float-finite-vc --no-exec-info;

# Additional generated examples kept in compact loops so the case list is visible.
FME_GE_COMMON=(-IQCP_examples/Applications_human/ -slp QCP_examples/Applications_human/ SimpleC.EE.Applications_human)
FME_GE_GMP_SLP=(-slp QCP_examples/Applications_human/fme_ge_gmp/gmp/ SimpleC.EE.Applications_human.fme_ge_gmp.gmp)
FME_GE_FME_SLP=("${FME_GE_GMP_SLP[@]}" -slp QCP_examples/Applications_human/fme_ge_gmp/fme/ SimpleC.EE.Applications_human.fme_ge_gmp.fme)
FME_GE_GE_SLP=("${FME_GE_GMP_SLP[@]}" -slp QCP_examples/Applications_human/fme_ge_gmp/ge/ SimpleC.EE.Applications_human.fme_ge_gmp.ge)

for strategy in gmp gmp_optional mpz_div_qr mpz_tdiv_r_read0; do
  linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/fme_ge_gmp/gmp/ --coq-logic-path=SimpleC.EE.Applications_human.fme_ge_gmp.gmp "${FME_GE_GMP_SLP[@]}" "${FME_GE_COMMON[@]}" --input-file=QCP_examples/Applications_human/fme_ge_gmp/gmp/${strategy}.strategies --no-exec-info
done
for strategy in fme_gmp safeexec_fme_gmp; do
  linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/fme_ge_gmp/fme/ --coq-logic-path=SimpleC.EE.Applications_human.fme_ge_gmp.fme "${FME_GE_FME_SLP[@]}" "${FME_GE_COMMON[@]}" --input-file=QCP_examples/Applications_human/fme_ge_gmp/fme/${strategy}.strategies --no-exec-info
done
for strategy in ge_gmp_array; do
  linux-binary/StrategyCheck --coq-output-dir=Rocq/examples/Applications_human/fme_ge_gmp/ge/ --coq-logic-path=SimpleC.EE.Applications_human.fme_ge_gmp.ge "${FME_GE_GE_SLP[@]}" "${FME_GE_COMMON[@]}" --input-file=QCP_examples/Applications_human/fme_ge_gmp/ge/${strategy}.strategies --no-exec-info
done

for case in gmp_clz gmp_udiv_qr_3by2 gmp_udiv_qrnnd_preinv mpn_add mpn_add_1 mpn_add_n mpn_addmul_1 mpn_div_qr mpn_div_qr_1_invert mpn_div_qr_1_preinv mpn_div_qr_2_invert mpn_div_qr_2_preinv mpn_div_qr_invert mpn_div_qr_pi1 mpn_div_qr_preinv mpn_gcd_11 mpn_invert_3by2 mpn_lshift mpn_mul mpn_rshift mpn_sub mpn_sub_1 mpn_sub_n mpn_submul_1 mpz_abs mpz_abs_add mpz_abs_sub mpz_add mpz_add_ui mpz_addmul mpz_cmp mpz_div_qr mpz_divexact mpz_gcd mpz_init mpz_init_set mpz_init_set_ui mpz_init2 mpz_make_odd mpz_mul mpz_mul_2exp mpz_mul_r_eq_op1 mpz_mul_r_eq_op2 mpz_neg mpz_set mpz_set_si mpz_set_ui mpz_sub mpz_sub_ui mpz_tdiv_q_2exp mpz_tdiv_r mpz_tdiv_r_read0 mpz_ui_sub mrz_realloc_if; do
  linux-binary/symexec --goal-file=Rocq/examples/Applications_human/fme_ge_gmp/gmp/${case}_goal.v --proof-auto-file=Rocq/examples/Applications_human/fme_ge_gmp/gmp/${case}_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/fme_ge_gmp/gmp/${case}_proof_manual.v --coq-logic-path=SimpleC.EE.Applications_human.fme_ge_gmp.gmp "${FME_GE_GMP_SLP[@]}" "${FME_GE_COMMON[@]}" --input-file=QCP_examples/Applications_human/fme_ge_gmp/gmp/${case}.c --no-exec-info
done
for case in fme_gmp; do
  linux-binary/symexec --goal-file=Rocq/examples/Applications_human/fme_ge_gmp/fme/${case}_goal.v --proof-auto-file=Rocq/examples/Applications_human/fme_ge_gmp/fme/${case}_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/fme_ge_gmp/fme/${case}_proof_manual.v --coq-logic-path=SimpleC.EE.Applications_human.fme_ge_gmp.fme "${FME_GE_FME_SLP[@]}" "${FME_GE_COMMON[@]}" --input-file=QCP_examples/Applications_human/fme_ge_gmp/fme/${case}.c --no-exec-info
done
for case in build_aug_basis_gmp build_inverse_cols_gmp col_swap_mod_gmp copy_vector_to_col_gmp gauss_solve_mod_gmp matrix_inverse_gmp mod_inv_gmp mod_norm_gmp rank_mod_gmp row_elim_mod_gmp row_scale_mod_gmp row_swap_mod_gmp solve_basis_into_col_gmp; do
  linux-binary/symexec --goal-file=Rocq/examples/Applications_human/fme_ge_gmp/ge/${case}_goal.v --proof-auto-file=Rocq/examples/Applications_human/fme_ge_gmp/ge/${case}_proof_auto.v --proof-manual-file=Rocq/examples/Applications_human/fme_ge_gmp/ge/${case}_proof_manual.v --coq-logic-path=SimpleC.EE.Applications_human.fme_ge_gmp.ge "${FME_GE_GE_SLP[@]}" "${FME_GE_COMMON[@]}" --input-file=QCP_examples/Applications_human/fme_ge_gmp/ge/${case}.c --no-exec-info
done

echo "All tests finished"