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/web/uclid_pb_benchmarks/normalized-ooo.unbounded.all.ucl.opb
MD5SUMe8f0ca38acbe8c57203147fb9147be3a
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 129
Number of bits of the biggest number in a constraint 8
Biggest sum of numbers in a constraint 510
Number of bits of the biggest sum of numbers9
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark487.167
Number of variables84836
Total number of constraints245062
Number of constraints which are clauses233598
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints11464
Minimum length of a constraint1
Maximum length of a constraint15

Trace number 40852 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-06-08 23:10:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=28918 boxname=wulflinc4 idbench=304 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  e8f0ca38acbe8c57203147fb9147be3a  /oldhome/oroussel/tmp/wulflinc4/normalized-ooo.unbounded.all.ucl.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc4/normalized-ooo.unbounded.all.ucl.opb
IDLAUNCH: 28918
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        909616 kB
Buffers:         28692 kB
Cached:          73332 kB
SwapCached:       2084 kB
Active:          30504 kB
Inactive:        74680 kB
HighTotal:      131008 kB
HighFree:        56868 kB
LowTotal:       903652 kB
LowFree:        852748 kB
SwapTotal:     2097136 kB
SwapFree:      2093984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4908 kB
Slab:            14020 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-08 23:13:51 (client local time) WITH STATUS 0 IN 230.796 SECONDS
stats: 28918 7 230.796 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c INFO: No cost function. Find solution and finish.
c Initial problem consists of 84836 variables and 245062 constraints.
#### 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.90 0.95 0.91 1/54 6312
Raw data (stat): 6312 (runsolver) R 6311 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 905475694 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0003 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 20931 0 0 0 949 48 0 0 25 0 1 0 905475694 43999232 7402 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10742 7406 1111 63 0 10679 0
vsize: 42968
[startup+20.0006 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 115186 0 0 0 1782 216 0 0 25 0 1 0 905475694 62107648 11851 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 15163 11859 1111 63 0 15100 0
vsize: 60652
[startup+30.0014 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 344895 0 0 0 2379 619 0 0 25 0 1 0 905475694 73216000 14508 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17875 14514 1111 63 0 17812 0
vsize: 71500
[startup+40.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 569011 0 0 0 2981 1017 0 0 25 0 1 0 905475694 82317312 16722 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 20097 16730 1111 63 0 20034 0
vsize: 80388
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 793731 0 0 0 3571 1427 0 0 25 0 1 0 905475694 90468352 18703 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 22087 18710 1111 63 0 22024 0
vsize: 88348
[startup+60.0039 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 1012789 0 0 0 4171 1827 0 0 25 0 1 0 905475694 97669120 20505 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 23845 20511 1111 63 0 23782 0
vsize: 95380
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 1228600 0 0 0 4774 2224 0 0 25 0 1 0 905475694 105201664 22356 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 25684 22363 1111 63 0 25621 0
vsize: 102736
[startup+80.0048 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 1442808 0 0 0 5371 2627 0 0 25 0 1 0 905475694 111321088 23822 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 27178 23828 1111 63 0 27115 0
vsize: 108712
[startup+90.0056 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 1653317 0 0 0 5980 3019 0 0 25 0 1 0 905475694 117157888 25281 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 28603 25288 1111 63 0 28540 0
vsize: 114412
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 1863756 0 0 0 6583 3415 0 0 25 0 1 0 905475694 123351040 26600 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 30115 26606 1111 63 0 30052 0
vsize: 120460
[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 2068646 0 0 0 7192 3807 0 0 25 0 1 0 905475694 128512000 27878 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 31375 27884 1111 63 0 31312 0
vsize: 125500
[startup+120.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 2273449 0 0 0 7806 4194 0 0 25 0 1 0 905475694 133406720 29049 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 32570 29056 1111 63 0 32507 0
vsize: 130280
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 2475862 0 0 0 8412 4587 0 0 25 0 1 0 905475694 138018816 30229 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 33696 30235 1111 63 0 33633 0
vsize: 134784
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 2676814 0 0 0 9018 4981 0 0 25 0 1 0 905475694 142503936 31318 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 34791 31324 1111 63 0 34728 0
vsize: 139164
[startup+150.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 2877752 0 0 0 9626 5374 0 0 25 0 1 0 905475694 146710528 32374 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 35818 32380 1111 63 0 35755 0
vsize: 143272
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 3078227 0 0 0 10236 5764 0 0 25 0 1 0 905475694 150925312 33347 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 36847 33352 1111 63 0 36784 0
vsize: 147388
[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 3175872 0 0 0 11029 5971 0 0 25 0 1 0 905475694 311984128 74550 4294967295 134512640 134716908 3221224560 3221223200 134606495 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 76168 74550 1111 63 0 76105 0
vsize: 304672
[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 3328676 0 0 0 11668 6331 0 0 25 0 1 0 905475694 321298432 76958 4294967295 134512640 134716908 3221224560 3221223128 134587990 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 78442 76958 1111 63 0 78379 0
vsize: 313768
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 3548582 0 0 0 12127 6872 0 0 25 0 1 0 905475694 444841984 107126 4294967295 134512640 134716908 3221224560 3221223288 134543552 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108604 107126 1111 63 0 108541 0
vsize: 434416
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 3670352 0 0 0 12837 7163 0 0 25 0 1 0 905475694 444841984 107135 4294967295 134512640 134716908 3221224560 3221222912 134543030 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108604 107135 1111 63 0 108541 0
vsize: 434416
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 3797597 0 0 0 13530 7470 0 0 25 0 1 0 905475694 454021120 109382 4294967295 134512640 134716908 3221224560 3221223312 134630814 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 110845 109382 1111 63 0 110782 0
vsize: 443380
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 3916875 0 0 0 14245 7755 0 0 25 0 1 0 905475694 480538624 115863 4294967295 134512640 134716908 3221224560 3221223024 134543097 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 117319 115863 1111 63 0 117256 0
vsize: 469276
[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 4133601 0 0 0 14722 8279 0 0 25 0 1 0 905475694 917192704 222282 4294967295 134512640 134716908 3221224560 3221223200 134606495 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 223924 222289 1111 63 0 223861 0
vsize: 895696
[startup+230.803 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 6312
Raw data (stat): 6312 (bsolo_lpr_cuts-) R 6311 21152 21151 0 -1 0 4133601 0 0 0 14722 8279 0 0 25 0 1 0 905475694 917192704 222282 4294967295 134512640 134716908 3221224560 3221223200 134606495 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 223924 222289 1111 63 0 223861 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 230.802
CPU time (s): 230.796
CPU user time (s): 147.395
CPU system time (s): 83.4013
CPU usage (%): 99.9972
Max. virtual memory (Kb): 895696
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####