Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namenormalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-sc50a.opb
MD5SUMd1a63d8d6fb70cfa129ffc4588721d0f
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 20
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 1048575
Number of bits of the sum of numbers in the objective function 20
Biggest number in a constraint 8388608
Number of bits of the biggest number in a constraint 24
Biggest sum of numbers in a constraint 22020075
Number of bits of the biggest sum of numbers25
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.19282
Number of variables960
Total number of constraints49
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints49
Minimum length of a constraint40
Maximum length of a constraint80

Trace number 27723 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-05-24 23:09:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16149 boxname=wulflinc9 idbench=1243 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  d1a63d8d6fb70cfa129ffc4588721d0f  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-sc50a.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-sc50a.opb
IDLAUNCH: 16149
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        835316 kB
Buffers:         22716 kB
Cached:         155900 kB
SwapCached:        360 kB
Active:          40224 kB
Inactive:       140924 kB
HighTotal:      131008 kB
HighFree:         8624 kB
LowTotal:       903652 kB
LowFree:        826692 kB
SwapTotal:     2097136 kB
SwapFree:      2096368 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6348 kB
Slab:            12492 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-24 23:15:17 (client local time) WITH STATUS 0 IN 363.301 SECONDS
stats: 16149 7 363.301 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Initial problem consists of 960 variables and 69 constraints.
c After prepocess the problem consists of 727 variables and 69 constraints.
c preprocess terminated 0.349 s
c Initial Lower Bound: -16383
c Lower Bound Elapsed time: 0
c Use computed LB before first solution.
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.64 0.85 0.87 2/54 11910
Raw data (stat): 11910 (runsolver) R 11909 3944 3943 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 775862134 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99988 s]
Raw data (loadavg): 0.69 0.85 0.87 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 8380 0 0 0 978 20 0 0 25 0 1 0 775862134 38178816 8316 4294967295 134512640 134714540 3221224592 3221223200 134543759 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9321 8316 1111 63 0 9258 0
vsize: 37284
[startup+20.0006 s]
Raw data (loadavg): 0.74 0.86 0.87 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 15424 0 0 0 1959 39 0 0 25 0 1 0 775862134 67182592 15262 4294967295 134512640 134714540 3221224592 3221223288 134558629 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16402 15262 1111 63 0 16339 0
vsize: 65608
[startup+30.0015 s]
Raw data (loadavg): 0.78 0.86 0.87 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 22351 0 0 0 2943 56 0 0 25 0 1 0 775862134 97280000 22018 4294967295 134512640 134714540 3221224592 3221223328 134556832 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 23750 22018 1111 63 0 23687 0
vsize: 95000
[startup+40.0012 s]
Raw data (loadavg): 0.81 0.87 0.87 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 28884 0 0 0 3923 75 0 0 25 0 1 0 775862134 122994688 28538 4294967295 134512640 134714540 3221224592 3221223336 134536879 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30028 28538 1111 63 0 29965 0
vsize: 120112
[startup+50.002 s]
Raw data (loadavg): 0.84 0.87 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 37386 0 0 0 4903 96 0 0 25 0 1 0 775862134 157896704 35400 4294967295 134512640 134714540 3221224592 3221223264 134553189 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 38549 35400 1111 63 0 38486 0
vsize: 154196
[startup+60.0018 s]
Raw data (loadavg): 0.87 0.87 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 42902 0 0 0 5886 112 0 0 25 0 1 0 775862134 179503104 40752 4294967295 134512640 134714540 3221224592 3221223308 134558476 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 43824 40752 1111 63 0 43761 0
vsize: 175296
[startup+70.0025 s]
Raw data (loadavg): 0.89 0.88 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 49349 0 0 0 6868 131 0 0 25 0 1 0 775862134 204779520 47199 4294967295 134512640 134714540 3221224592 3221223240 134543652 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 49995 47199 1111 63 0 49932 0
vsize: 199980
[startup+80.0033 s]
Raw data (loadavg): 0.90 0.88 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 56208 0 0 0 7851 148 0 0 25 0 1 0 775862134 231030784 53753 4294967295 134512640 134714540 3221224592 3221223428 134623280 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 56404 53753 1111 63 0 56341 0
vsize: 225616
[startup+90.003 s]
Raw data (loadavg): 0.92 0.88 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 62106 0 0 0 8835 164 0 0 25 0 1 0 775862134 254279680 59651 4294967295 134512640 134714540 3221224592 3221222920 1077378037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 62080 59651 1111 63 0 62017 0
vsize: 248320
[startup+100.003 s]
Raw data (loadavg): 0.93 0.89 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 74143 0 0 0 9809 190 0 0 25 0 1 0 775862134 299102208 67071 4294967295 134512640 134714540 3221224592 3221223132 134539296 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 73023 67071 1111 63 0 72960 0
vsize: 292092
[startup+110.033 s]
Raw data (loadavg): 0.94 0.89 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 80748 0 0 0 10795 207 0 0 25 0 1 0 775862134 324767744 73514 4294967295 134512640 134714540 3221224592 3221223328 134556547 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 79289 73514 1111 63 0 79226 0
vsize: 317156
[startup+120.041 s]
Raw data (loadavg): 0.95 0.89 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 84706 0 0 0 11785 218 0 0 25 0 1 0 775862134 340021248 77310 4294967295 134512640 134714540 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 83013 77310 1111 63 0 82950 0
vsize: 332052
[startup+130.042 s]
Raw data (loadavg): 0.96 0.90 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 91206 0 0 0 12767 236 0 0 25 0 1 0 775862134 365432832 83810 4294967295 134512640 134714540 3221224592 3221223336 134536879 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 89217 83810 1111 63 0 89154 0
vsize: 356868
[startup+140.041 s]
Raw data (loadavg): 0.96 0.90 0.88 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 97393 0 0 0 13752 251 0 0 25 0 1 0 775862134 389632000 89997 4294967295 134512640 134714540 3221224592 3221223296 134556773 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 95125 89997 1111 63 0 95062 0
vsize: 380500
[startup+150.042 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 105067 0 0 0 14733 269 0 0 25 0 1 0 775862134 416677888 96701 4294967295 134512640 134714540 3221224592 3221223216 134535468 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 101728 96701 1111 63 0 101665 0
vsize: 406912
[startup+160.042 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 111519 0 0 0 15713 290 0 0 25 0 1 0 775862134 441819136 103153 4294967295 134512640 134714540 3221224592 3221223296 134556899 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 107866 103153 1111 63 0 107803 0
vsize: 431464
[startup+170.042 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 117679 0 0 0 16698 305 0 0 25 0 1 0 775862134 465879040 109313 4294967295 134512640 134714540 3221224592 3221223232 134613454 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 113740 109313 1111 63 0 113677 0
vsize: 454960
[startup+180.042 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 122813 0 0 0 17683 321 0 0 25 0 1 0 775862134 485883904 114447 4294967295 134512640 134714540 3221224592 3221223328 134556887 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 118624 114447 1111 63 0 118561 0
vsize: 474496
[startup+190.042 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 129252 0 0 0 18663 340 0 0 25 0 1 0 775862134 511029248 120886 4294967295 134512640 134714540 3221224592 3221223160 1077377574 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 124763 120886 1111 63 0 124700 0
vsize: 499052
[startup+200.043 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 147110 0 0 0 19625 378 0 0 25 0 1 0 775862134 574742528 129084 4294967295 134512640 134714540 3221224592 3221223120 1076648080 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 140318 129084 1111 63 0 140255 0
vsize: 561272
[startup+210.042 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 153272 0 0 0 20607 396 0 0 25 0 1 0 775862134 598491136 134924 4294967295 134512640 134714540 3221224592 3221223340 134556933 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 146116 134924 1111 63 0 146053 0
vsize: 584464
[startup+220.05 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 160121 0 0 0 21590 414 0 0 25 0 1 0 775862134 625078272 141451 4294967295 134512640 134714540 3221224592 3221223488 134621515 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 152607 141451 1111 63 0 152544 0
vsize: 610428
[startup+230.05 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 166011 0 0 0 22571 433 0 0 25 0 1 0 775862134 648056832 147341 4294967295 134512640 134714540 3221224592 3221223304 134558561 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 158217 147341 1111 63 0 158154 0
vsize: 632868
[startup+240.05 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 169509 0 0 0 23561 443 0 0 25 0 1 0 775862134 661262336 150517 4294967295 134512640 134714540 3221224592 3221223248 134543740 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 161441 150517 1111 63 0 161378 0
vsize: 645764
[startup+250.05 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 173531 0 0 0 24550 455 0 0 25 0 1 0 775862134 676941824 154539 4294967295 134512640 134714540 3221224592 3221223292 134558630 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 165269 154539 1111 63 0 165206 0
vsize: 661076
[startup+260.05 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 179497 0 0 0 25534 470 0 0 25 0 1 0 775862134 700190720 160505 4294967295 134512640 134714540 3221224592 3221223292 134558620 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 170945 160505 1111 63 0 170882 0
vsize: 683780
[startup+270.051 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 185646 0 0 0 26515 489 0 0 25 0 1 0 775862134 724250624 166654 4294967295 134512640 134714540 3221224592 3221223368 134624400 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 176819 166654 1111 63 0 176756 0
vsize: 707276
[startup+280.051 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 191391 0 0 0 27499 505 0 0 25 0 1 0 775862134 746688512 172399 4294967295 134512640 134714540 3221224592 3221223336 134536877 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 182297 172399 1111 63 0 182234 0
vsize: 729188
[startup+290.051 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 197314 0 0 0 28482 522 0 0 25 0 1 0 775862134 769802240 178322 4294967295 134512640 134714540 3221224592 3221223312 134556674 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 187940 178322 1111 63 0 187877 0
vsize: 751760
[startup+300.051 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 203447 0 0 0 29465 540 0 0 25 0 1 0 775862134 793726976 184455 4294967295 134512640 134714540 3221224592 3221223336 134536872 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 193781 184455 1111 63 0 193718 0
vsize: 775124
[startup+310.051 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 211891 0 0 0 30443 562 0 0 25 0 1 0 775862134 820944896 190969 4294967295 134512640 134714540 3221224592 3221223328 134556832 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 200426 190969 1111 63 0 200363 0
vsize: 801704
[startup+320.052 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 217833 0 0 0 31426 579 0 0 25 0 1 0 775862134 844193792 196911 4294967295 134512640 134714540 3221224592 3221223312 134556924 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 206102 196911 1111 63 0 206039 0
vsize: 824408
[startup+330.053 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 224061 0 0 0 32409 596 0 0 25 0 1 0 775862134 868524032 203139 4294967295 134512640 134714540 3221224592 3221223312 134556640 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 212042 203139 1111 63 0 211979 0
vsize: 848168
[startup+340.053 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 229673 0 0 0 33393 611 0 0 25 0 1 0 775862134 890421248 208751 4294967295 134512640 134714540 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 217388 208751 1111 63 0 217325 0
vsize: 869552
[startup+350.053 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 235582 0 1 0 34373 630 0 0 25 0 1 0 775862134 913399808 214550 4294967295 134512640 134714540 3221224592 3221223312 134556843 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 222998 214550 1111 63 0 222935 0
vsize: 891992
[startup+360.054 s]
Raw data (loadavg): 1.07 0.96 0.91 2/54 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 242131 0 43 0 35331 654 0 0 25 0 1 0 775862134 937189376 220199 4294967295 134512640 134714540 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 228806 220199 1111 63 0 228743 0
vsize: 915224
[startup+363.704 s]
Raw data (loadavg): 1.07 0.96 0.91 1/53 11910
Raw data (stat): 11910 (bsolo_mis) R 11909 3944 3943 0 -1 0 242131 0 43 0 35331 654 0 0 25 0 1 0 775862134 937189376 220199 4294967295 134512640 134714540 3221224592 3221223516 1077781665 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 228806 220199 1111 63 0 228743 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 363.704
CPU time (s): 363.301
CPU user time (s): 356.265
CPU system time (s): 7.03593
CPU usage (%): 99.8891
Max. virtual memory (Kb): 915224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####