PB'05 competition: run trace

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:

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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/web/uclid_pb_benchmarks/normalized-ooo.ex.br.mem.Src1Valid_Src1ValidBar.ucl.opb
MD5SUM	46f4eb904b1c96b45521a6459aa5d49d
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable
(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	130
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	512
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	109757
Total number of constraints	313451
Number of constraints which are clauses	295929
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	17522
Minimum length of a constraint	1
Maximum length of a constraint	15

Trace number 39656

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-06-07 15:48:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=27721 boxname=wulflinc4 idbench=279 idsolver=20 numberseed=0
MD5SUM SOLVER: f6aa7fb267fa9710116626be7e6d3048  /oldhome/oroussel/solvers/bsolo_lpr-v2
MD5SUM BENCH:  46f4eb904b1c96b45521a6459aa5d49d  /oldhome/oroussel/tmp/wulflinc4/normalized-ooo.ex.br.mem.Src1Valid_Src1ValidBar.ucl.opb
REAL COMMAND:  bsolo_lpr-v2 /oldhome/oroussel/tmp/wulflinc4/normalized-ooo.ex.br.mem.Src1Valid_Src1ValidBar.ucl.opb
IDLAUNCH: 27721
/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:        368544 kB
Buffers:         35128 kB
Cached:         606700 kB
SwapCached:        568 kB
Active:          68608 kB
Inactive:       575352 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        368292 kB
SwapTotal:     2097136 kB
SwapFree:      2095660 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5328 kB
Slab:            16488 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-07 15:53:17 (client local time) WITH STATUS 0 IN 299.665 SECONDS
stats: 27721 7 299.665 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 109757 variables and 313451 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.85 0.95 0.93 1/54 17606
Raw data (stat): 17606 (runsolver) R 17605 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 894183953 884736 94 4294967295 134512640 135332820 3221224432 3221219612 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.0011 s]
Raw data (loadavg): 0.87 0.95 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 29447 0 0 0 933 64 0 0 25 0 1 0 894183953 40833024 6677 4294967295 134512640 134716908 3221224544 3221221308 1077191430 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9969 6677 1111 63 0 9906 0
vsize: 39876
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.95 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 124814 0 0 0 1753 244 0 0 25 0 1 0 894183953 56459264 10478 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 13784 10478 1111 63 0 13721 0
vsize: 55136
[startup+30.0024 s]
Raw data (loadavg): 0.91 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 351749 0 0 0 2359 638 0 0 25 0 1 0 894183953 67420160 13050 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 16460 13050 1111 63 0 16397 0
vsize: 65840
[startup+40.0037 s]
Raw data (loadavg): 0.92 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 573502 0 0 0 2967 1030 0 0 25 0 1 0 894183953 76386304 15251 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18649 15251 1111 63 0 18586 0
vsize: 74596
[startup+50.0051 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 792831 0 0 0 3565 1432 0 0 25 0 1 0 894183953 84258816 17205 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20571 17205 1111 63 0 20508 0
vsize: 82284
[startup+60.0049 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 1007543 0 0 0 4177 1821 0 0 25 0 1 0 894183953 91455488 18941 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 22328 18941 1111 63 0 22265 0
vsize: 89312
[startup+70.0053 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 1224198 0 0 0 4775 2223 0 0 25 0 1 0 894183953 98828288 20785 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 24128 20785 1111 63 0 24065 0
vsize: 96512
[startup+80.0057 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 1435802 0 0 0 5373 2625 0 0 25 0 1 0 894183953 104943616 22257 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 25621 22257 1111 63 0 25558 0
vsize: 102484
[startup+90.0055 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 1645211 0 0 0 5986 3012 0 0 25 0 1 0 894183953 110645248 23677 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 27013 23677 1111 63 0 26950 0
vsize: 108052
[startup+100.007 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 1857058 0 0 0 6582 3417 0 0 25 0 1 0 894183953 116211712 25049 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 28372 25055 1111 63 0 28309 0
vsize: 113488
[startup+110.007 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 2068933 0 0 0 7182 3817 0 0 25 0 1 0 894183953 122146816 26290 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29821 26296 1111 63 0 29758 0
vsize: 119284
[startup+120.007 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 2278721 0 0 0 7785 4214 0 0 25 0 1 0 894183953 127172608 27570 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30975 27502 1111 63 0 30912 0
vsize: 124192
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 2486603 0 0 0 8389 4610 0 0 25 0 1 0 894183953 131932160 28727 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 32210 28733 1111 63 0 32147 0
vsize: 128840
[startup+140.008 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 2691855 0 0 0 8992 5007 0 0 25 0 1 0 894183953 136409088 29785 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 33303 29791 1111 63 0 33240 0
vsize: 133212
[startup+150.008 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 2895527 0 0 0 9605 5394 0 0 25 0 1 0 894183953 140898304 30909 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 34399 30914 1111 63 0 34336 0
vsize: 137596
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 3095033 0 0 0 10208 5791 0 0 25 0 1 0 894183953 144969728 31932 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 35393 31938 1111 63 0 35330 0
vsize: 141572
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 3296005 0 0 0 10819 6180 0 0 25 0 1 0 894183953 149176320 32982 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 36420 32987 1111 63 0 36357 0
vsize: 145680
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 3496046 0 0 0 11427 6573 0 0 25 0 1 0 894183953 153128960 33880 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 37385 33886 1111 63 0 37322 0
vsize: 149540
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 3694595 0 0 0 12042 6958 0 0 25 0 1 0 894183953 156930048 34827 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 38313 34833 1111 63 0 38250 0
vsize: 153252
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 3892816 0 0 0 12654 7345 0 0 25 0 1 0 894183953 160600064 35782 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 39209 35788 1111 63 0 39146 0
vsize: 156836
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 4089906 0 0 0 13269 7731 0 0 25 0 1 0 894183953 164265984 36654 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 40104 36660 1111 63 0 40041 0
vsize: 160416
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 4285312 0 0 0 13878 8122 0 0 25 0 1 0 894183953 167796736 37538 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 40966 37543 1111 63 0 40903 0
vsize: 163864
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 4481071 0 0 0 14505 8495 0 0 25 0 1 0 894183953 171196416 38399 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 41796 38405 1111 63 0 41733 0
vsize: 167184
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 4677289 0 0 0 15121 8880 0 0 25 0 1 0 894183953 174592000 39171 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 42625 39177 1111 63 0 42562 0
vsize: 170500
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 4873229 0 0 0 15736 9265 0 0 25 0 1 0 894183953 177852416 40035 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 43421 40040 1111 63 0 43358 0
vsize: 173684
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 5066399 0 0 0 16350 9651 0 0 25 0 1 0 894183953 180981760 40822 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 44185 40827 1111 63 0 44122 0
vsize: 176740
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 5258576 0 0 0 16971 10030 0 0 25 0 1 0 894183953 184238080 41607 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 44875 41503 1111 63 0 44812 0
vsize: 179920
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 5450071 0 0 0 17584 10417 0 0 25 0 1 0 894183953 189054976 42705 4294967295 134512640 134716908 3221224544 3221222848 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 46156 42711 1111 63 0 46093 0
vsize: 184624
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 0 5519507 0 0 0 18446 10555 0 0 25 0 1 0 894183953 207138816 47215 4294967295 134512640 134716908 3221224544 3221223076 1077374149 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 50571 47215 1111 63 0 50508 0
vsize: 202284
[startup+300.387 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 1028 5701032 0 2 0 18910 11034 0 0 24 0 1 0 894183953 0 0 4294967295 0 0 0 0 0 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
[startup+300.503 s]
Raw data (loadavg): 0.99 0.97 0.93 1/53 17606
Raw data (stat): 17606 (bsolo_lpr-v2) R 17605 21152 21151 0 -1 1028 5701032 0 2 0 18910 11034 0 0 24 0 1 0 894183953 0 0 4294967295 0 0 0 0 0 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 300.503
CPU time (s): 299.665
CPU user time (s): 189.103
CPU system time (s): 110.562
CPU usage (%): 99.7214
Max. virtual memory (Kb): 202284
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####