### uname -a: Linux clpc8.cs.ox.ac.uk 2.6.34.7-56.fc13.x86_64 #1 SMP Wed Sep 15 03:36:55 UTC 2010 x86_64 x86_64 x86_64 GNU/Linux ### cat /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 0 cpu cores : 4 apicid : 0 initial apicid : 0 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5653.20 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 1 cpu cores : 4 apicid : 1 initial apicid : 1 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5652.19 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: processor : 2 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 2 cpu cores : 4 apicid : 2 initial apicid : 2 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5652.20 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: processor : 3 vendor_id : GenuineIntel cpu family : 6 model : 23 model name : Intel(R) Core(TM)2 Quad CPU Q9550 @ 2.83GHz stepping : 10 cpu MHz : 2826.601 cache size : 6144 KB physical id : 0 siblings : 4 core id : 3 cpu cores : 4 apicid : 3 initial apicid : 3 fpu : yes fpu_exception : yes cpuid level : 13 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx lm constant_tsc arch_perfmon pebs bts rep_good aperfmperf pni dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm sse4_1 xsave lahf_lm tpr_shadow vnmi flexpriority bogomips : 5652.21 clflush size : 64 cache_alignment : 64 address sizes : 36 bits physical, 48 bits virtual power management: ### cat /proc/meminfo: MemTotal: 3891428 kB MemFree: 3434100 kB Buffers: 6124 kB Cached: 58032 kB SwapCached: 3960 kB Active: 216016 kB Inactive: 55584 kB Active(anon): 201564 kB Inactive(anon): 47656 kB Active(file): 14452 kB Inactive(file): 7928 kB Unevictable: 0 kB Mlocked: 0 kB SwapTotal: 12586892 kB SwapFree: 12517592 kB Dirty: 1068 kB Writeback: 0 kB AnonPages: 205448 kB Mapped: 7568 kB Shmem: 41848 kB Slab: 47512 kB SReclaimable: 29612 kB SUnreclaim: 17900 kB KernelStack: 2080 kB PageTables: 13140 kB NFS_Unstable: 0 kB Bounce: 0 kB WritebackTmp: 0 kB CommitLimit: 14532604 kB Committed_AS: 674920 kB VmallocTotal: 34359738367 kB VmallocUsed: 385656 kB VmallocChunk: 34359345788 kB HardwareCorrupted: 0 kB HugePages_Total: 0 HugePages_Free: 0 HugePages_Rsvd: 0 HugePages_Surp: 0 Hugepagesize: 2048 kB DirectMap4k: 10236 kB DirectMap2M: 4016128 kB ### date: Fri Oct 14 01:06:17 BST 2011 ### user: mictau ### ulimit -a: core file size (blocks, -c) 0 data seg size (kbytes, -d) unlimited scheduling priority (-e) 0 file size (blocks, -f) unlimited pending signals (-i) 30273 max locked memory (kbytes, -l) 64 max memory size (kbytes, -m) unlimited open files (-n) 1024 pipe size (512 bytes, -p) 8 POSIX message queues (bytes, -q) 819200 real-time priority (-r) 0 stack size (kbytes, -s) 10240 cpu time (seconds, -t) unlimited max user processes (-u) 1024 virtual memory (kbytes, -v) 3584000 file locks (-x) unlimited ### timeout: timeout -s SIGINT 3600 ### tool version info: 4.0 ### tool command: cbmc ### full command line: cbmc /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/build/other/sac_ga/sac.0.60.i ### expected verification result: unknown ############################################################################### file /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/build/other/sac_ga/sac.0.60.i: Parsing Converting Type-checking sac.0.60 Generating GOTO Program Adding CPROVER library Function Pointer Removal Partial Inlining Generic Property Instrumentation Starting Bounded Model Checking **** WARNING: no body for function c::nondetSING **** WARNING: no body for function c::nondetUINT8 Unwinding loop c::main.0 iteration 1 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 2 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 3 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 4 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 5 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 6 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 7 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 8 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 9 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 10 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 11 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 12 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 13 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 14 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 15 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 16 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 17 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 18 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 19 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 20 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 21 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 22 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 23 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 24 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 25 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 26 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 27 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 28 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 29 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 30 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 31 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 32 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 33 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 34 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 35 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 36 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 37 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 38 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 39 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 40 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 41 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 42 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 43 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 44 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 45 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 46 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 47 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 48 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 49 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 50 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 51 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 52 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 53 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 54 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 55 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 56 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 57 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 58 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 59 file other/sac_ga/sac.c line 796 function main Unwinding loop c::main.0 iteration 60 file other/sac_ga/sac.c line 796 function main size of program expression: 31114 assignments simple slicing removed 5 assignments Generated 60 VCC(s), 60 remaining after simplification Passing problem to propositional reduction terminate called after throwing an instance of 'Minisat::OutOfMemoryException' ############################################################################### ### exit code: 0 ### /usr/bin/time -v: Command being timed: "cbmc /home/scratch/mictau/cprover-benchmarking.git/tmp/cdfpl/build/other/sac_ga/sac.0.60.i" User time (seconds): 132.08 System time (seconds): 3.83 Percent of CPU this job got: 73% Elapsed (wall clock) time (h:mm:ss or m:ss): 3:05.11 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 3186264 Average resident set size (kbytes): 0 Major (requiring I/O) page faults: 61 Minor (reclaiming a frame) page faults: 881491 Voluntary context switches: 654621 Involuntary context switches: 1326 Swaps: 0 File system inputs: 11824 File system outputs: 1184 Socket messages sent: 0 Socket messages received: 0 Signals delivered: 0 Page size (bytes): 4096 Exit status: 0