Tool CPAchecker 1.7-svn 27742
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
OS Linux 4.4.0-121-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Run set kInduction-df-boxes kInduction-df-boxes+eq kInduction-df-boxes+eq+mod2 kInduction-kipdr
Options -noout -heap 10000M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -kInduction -setprop cpa.invariants.conditionAdjusterFactory=STATIC -setprop cpa.invariants.interestingVariableLimit=0 -setprop cpa.invariants.maximumFormulaDepth=0 -setprop cpa.invariants.abstractionStateFactory=ENTERING_EDGES -noout -heap 10000M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -kInduction -setprop cpa.invariants.conditionAdjusterFactory=STATIC -setprop cpa.invariants.interestingVariableLimit=0 -setprop cpa.invariants.maximumFormulaDepth=1 -setprop cpa.invariants.abstractionStateFactory=ENTERING_EDGES -setprop cpa.invariants.useMod2Template=false -noout -heap 10000M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -kInduction -setprop cpa.invariants.conditionAdjusterFactory=STATIC -setprop cpa.invariants.interestingVariableLimit=0 -setprop cpa.invariants.maximumFormulaDepth=1 -setprop cpa.invariants.abstractionStateFactory=ENTERING_EDGES -setprop cpa.invariants.useMod2Template=true -noout -heap 10000M -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -kInduction-kipdrInvariants
../programs/pdr/ status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) memUsage host
const.c true 3.26 1.80 251617280 apollon099 true 3.25 1.82 255578112 apollon115 true 3.16 1.78 249749504 apollon123 true 3.77 2.10 287895552 apollon149
eq1.c timeout 928    924    775389184 apollon149 true 3.15 1.77 254009344 apollon125 true 3.32 1.83 255787008 apollon164 true 4.91 2.71 305012736 apollon007
eq2.c out of memory 786    773    14999998464 apollon090 out of memory 794    781    14999998464 apollon158 out of memory 790    777    14999998464 apollon143 true 3.91 2.17 282636288 apollon149
even.c timeout 914    900    13089226752 apollon106 timeout 914    900    12499185664 apollon128 true 3.46 1.93 261636096 apollon115 true 3.90 2.14 284737536 apollon074
odd.c timeout 911    896    11391614976 apollon155 timeout 913    898    11975262208 apollon123 true 3.42 1.93 259272704 apollon122 true 4.13 2.24 306159616 apollon088
mod4.c timeout 915    900    12301144064 apollon042 timeout 912    896    11503665152 apollon150 timeout 914    900    11758108672 apollon014 true 3.57 2.02 278380544 apollon121
bin-suffix-5.c out of memory 798    783    14999998464 apollon058 out of memory 853    836    14999998464 apollon147 out of memory 802    787    14999998464 apollon127 true 3.62 2.03 279654400 apollon121
../programs/pdr/ status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) memUsage host status cputime (s) walltime (s) memUsage host
total 7 5260 5180 67808989184 7 4390 4310 66487697408 7 2520 2470 42784550912 7 27.8 15.4 2024476672
local summary 945 945 945 945  
    correct results 0 0 0 0
        correct true 0 0 0 0
        correct false 0 0 0 0
    incorrect results 0 0 0 0
        incorrect true 0 0 0 0
        incorrect false 0 0 0 0
Run set kInduction-df-boxes kInduction-df-boxes+eq kInduction-df-boxes+eq+mod2 kInduction-kipdr