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-cache-ibm-q-full.all.ucl.opb
MD5SUMb8424149645ffb0af409a9e7aef74685
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
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 68
Number of bits of the biggest number in a constraint 7
Biggest sum of numbers in a constraint 257
Number of bits of the biggest sum of numbers9
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables81558
Total number of constraints240469
Number of constraints which are clauses235865
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints4604
Minimum length of a constraint1
Maximum length of a constraint13

Trace number 24492 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-10 18:33:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2431 boxname=wulflinc31 idbench=271 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  b8424149645ffb0af409a9e7aef74685  /oldhome/oroussel/tmp/wulflinc31/normalized-cache-ibm-q-full.all.ucl.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc31/normalized-cache-ibm-q-full.all.ucl.opb
IDLAUNCH: 2431
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        271648 kB
Buffers:         47344 kB
Cached:         680904 kB
SwapCached:        644 kB
Active:         322116 kB
Inactive:       408432 kB
HighTotal:      131008 kB
HighFree:         9632 kB
LowTotal:       903652 kB
LowFree:        262016 kB
SwapTotal:     2097892 kB
SwapFree:      2096612 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5608 kB
Slab:            26680 kB
Committed_AS:    63632 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-10 18:39:02 (client local time) WITH STATUS 0 IN 297.985 SECONDS
stats: 2431 7 297.985 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 81558 variables and 240469 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
Raw data (loadavg): 0.80 0.87 0.88 2/54 15061
Raw data (stat): 15061 (runsolver) D 15060 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 711439188 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 2147483391 1 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0009 s]
Raw data (loadavg): 0.83 0.87 0.88 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 14291 0 0 0 958 38 0 0 25 0 1 0 711439188 46907392 8113 4294967295 134512640 134714508 3221221776 3221219820 1077386340 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 11452 8118 1111 63 0 11389 0
vsize: 45808
[startup+20.0013 s]
Raw data (loadavg): 0.86 0.88 0.88 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 82525 0 0 0 1827 168 0 0 25 0 1 0 711439188 64811008 12545 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 15884 12546 1111 63 0 15821 0
vsize: 63292
[startup+30.0015 s]
Raw data (loadavg): 0.88 0.88 0.88 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 277900 0 0 0 2487 508 0 0 25 0 1 0 711439188 76476416 15319 4294967295 134512640 134714508 3221221776 3221220008 1077378037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18709 15322 1111 63 0 18646 0
vsize: 74684
[startup+40.0025 s]
Raw data (loadavg): 0.90 0.89 0.88 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 502156 0 0 0 3098 898 0 0 25 0 1 0 711439188 85999616 17644 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 20953 17602 1111 63 0 20890 0
vsize: 83984
[startup+50.0032 s]
Raw data (loadavg): 0.91 0.89 0.88 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 723501 0 0 0 3702 1293 0 0 25 0 1 0 711439188 93954048 19605 4294967295 134512640 134714508 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 22938 19606 1111 63 0 22875 0
vsize: 91752
[startup+60.0043 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 941784 0 0 0 4309 1686 0 0 25 0 1 0 711439188 101482496 21419 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 24776 21425 1111 63 0 24713 0
vsize: 99104
[startup+70.0043 s]
Raw data (loadavg): 0.94 0.89 0.89 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 1160672 0 0 0 4918 2077 0 0 25 0 1 0 711439188 109150208 23299 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 26648 23305 1111 63 0 26585 0
vsize: 106592
[startup+80.0039 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 1373878 0 0 0 5525 2471 0 0 25 0 1 0 711439188 115400704 24847 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 28174 24852 1111 63 0 28111 0
vsize: 112696
[startup+90.0042 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 1585243 0 0 0 6132 2864 0 0 25 0 1 0 711439188 121110528 26246 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 29568 26251 1111 63 0 29505 0
vsize: 118272
[startup+100.004 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 1791294 0 0 0 6738 3257 0 0 25 0 1 0 711439188 127303680 27589 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 31080 27595 1111 63 0 31017 0
vsize: 124320
[startup+110.005 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 2000578 0 0 0 7347 3649 0 0 25 0 1 0 711439188 132599808 28850 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 32373 28855 1111 63 0 32310 0
vsize: 129492
[startup+120.006 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 2206462 0 0 0 7958 4037 0 0 25 0 1 0 711439188 137490432 30083 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 33567 30088 1111 63 0 33504 0
vsize: 134268
[startup+130.006 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 2409040 0 0 0 8567 4429 0 0 25 0 1 0 711439188 141803520 31189 4294967295 134512640 134714508 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 34620 31189 1111 63 0 34557 0
vsize: 138480
[startup+140.007 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 2611625 0 0 0 9189 4807 0 0 25 0 1 0 711439188 146591744 32336 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 35789 32341 1111 63 0 35726 0
vsize: 143156
[startup+150.007 s]
Raw data (loadavg): 1.06 0.93 0.90 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 2812838 0 0 0 9798 5198 0 0 25 0 1 0 711439188 150941696 33378 4294967295 134512640 134714508 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 36851 33383 1111 63 0 36788 0
vsize: 147404
[startup+160.008 s]
Raw data (loadavg): 1.05 0.93 0.90 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 2960608 0 0 0 10454 5539 0 0 25 0 1 0 711439188 274817024 65626 4294967295 134512640 134714508 3221221776 3221220256 134536630 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 67094 65626 1111 63 0 67031 0
vsize: 268376
[startup+170.009 s]
Raw data (loadavg): 1.04 0.94 0.90 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 3138783 0 0 0 11002 5988 0 0 25 0 1 0 711439188 409493504 98361 4294967295 134512640 134714508 3221221776 3221220416 134606468 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 99974 98361 1111 63 0 99911 0
vsize: 399896
[startup+180.01 s]
Raw data (loadavg): 1.04 0.94 0.90 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 3286174 0 31 0 11427 6387 0 0 25 0 1 0 711439188 505831424 120354 4294967295 134512640 134714508 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 123494 120354 1111 63 0 123431 0
vsize: 493976
[startup+190.011 s]
Raw data (loadavg): 1.03 0.94 0.90 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 3408202 0 42 0 12093 6711 0 0 25 0 1 0 711439188 529555456 125973 4294967295 134512640 134714508 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 129286 125973 1111 63 0 129223 0
vsize: 517144
[startup+200.01 s]
Raw data (loadavg): 1.02 0.94 0.90 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 3525317 0 44 0 12765 7036 0 0 25 0 1 0 711439188 506945536 120680 4294967295 134512640 134714508 3221221776 3221220256 134539374 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 123766 120680 1111 63 0 123703 0
vsize: 495064
[startup+210.012 s]
Raw data (loadavg): 1.02 0.94 0.91 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 3627346 0 44 0 13497 7305 0 0 25 0 1 0 711439188 523657216 124545 4294967295 134512640 134714508 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 127846 124551 1111 63 0 127783 0
vsize: 511384
[startup+220.012 s]
Raw data (loadavg): 1.02 0.94 0.91 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 3729824 0 45 0 14221 7579 0 0 25 0 1 0 711439188 502030336 119502 4294967295 134512640 134714508 3221221776 3221220140 134539237 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 122566 119502 1111 63 0 122503 0
vsize: 490264
[startup+230.012 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 3864233 0 45 0 14863 7937 0 0 25 0 1 0 711439188 502161408 119510 4294967295 134512640 134714508 3221221776 3221220140 134539235 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 122598 119510 1111 63 0 122535 0
vsize: 490392
[startup+240.014 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 3976483 0 46 0 15558 8240 0 0 25 0 1 0 711439188 551313408 131432 4294967295 134512640 134714508 3221221776 3221220416 134606479 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 134598 131432 1111 63 0 134535 0
vsize: 538392
[startup+250.014 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 4102870 0 49 0 16213 8581 0 0 25 0 1 0 711439188 502161408 119569 4294967295 134512640 134714508 3221221776 3221220240 134542300 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 122598 119569 1111 63 0 122535 0
vsize: 490392
[startup+260.015 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 4225055 0 53 0 16881 8907 0 0 25 0 1 0 711439188 546398208 130392 4294967295 134512640 134714508 3221221776 3221220516 134630783 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 133398 130392 1111 63 0 133335 0
vsize: 533592
[startup+270.015 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 4304509 0 53 0 17670 9118 0 0 25 0 1 0 711439188 527720448 125842 4294967295 134512640 134714508 3221221776 3221220504 134672913 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 128838 125842 1111 63 0 128775 0
vsize: 515352
[startup+280.015 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 4420207 0 55 0 18364 9421 0 0 25 0 1 0 711439188 529821696 126333 4294967295 134512640 134714508 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 129351 126339 1111 63 0 129288 0
vsize: 517404
[startup+290.016 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 15061
Raw data (stat): 15061 (bsolo_lpr) R 15060 7876 7672 0 -1 0 4571268 0 55 0 18973 9812 0 0 25 0 1 0 711439188 676294656 161948 4294967295 134512640 134714508 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 165111 161954 1111 63 0 165048 0
vsize: 660444
[startup+300.017 s]
Raw data (loadavg): 1.00 0.95 0.91 1/54 15061
Raw data (stat): 15061 (bsolo_lpr) D 15060 7876 7672 0 -1 2048 4764581 0 57 0 19361 10303 0 0 24 0 1 0 711439188 871071744 206714 4294967295 134512640 134714508 3221221776 3221220304 134554866 0 0 1 0 3223805148 0 0 17 1 0 0
Raw data (statm): 212664 206714 1111 63 0 212601 0
vsize: 850656
[startup+305.39 s]
Raw data (loadavg): 1.24 1.00 0.93 1/53 15061
Raw data (stat): 15061 (bsolo_lpr) D 15060 7876 7672 0 -1 2048 4764581 0 57 0 19361 10303 0 0 24 0 1 0 711439188 871071744 206714 4294967295 134512640 134714508 3221221776 3221220304 134554866 0 0 1 0 3223805148 0 0 17 1 0 0
Raw data (statm): 212664 206714 1111 63 0 212601 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 305.389
CPU time (s): 297.985
CPU user time (s): 193.982
CPU system time (s): 104.003
CPU usage (%): 97.5754
Max. virtual memory (Kb): 850656
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####