Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
-V- |
{{line.desc}}
|
1 | extern void __VERIFIER_error() __attribute__ ((__noreturn__)); |
2 | void __VERIFIER_assert(int cond) { |
3 | if (!(cond)) { |
4 | ERROR: __VERIFIER_error(); |
5 | } |
6 | return; |
7 | } |
8 | extern int __VERIFIER_nondet_uint(); |
9 | |
10 | int main(void) { |
11 | unsigned int w = __VERIFIER_nondet_uint(); |
12 | unsigned int x = w; |
13 | unsigned int y = w + 1; |
14 | unsigned int z = x + 1; |
15 | while (__VERIFIER_nondet_uint()) { |
16 | y++; |
17 | z++; |
18 | } |
19 | __VERIFIER_assert(y == z); |
20 | return 0; |
21 | } |
2018-05-19 21:41:05:573 INFO CPAchecker.run CPAchecker 1.7-svn (Java HotSpot(TM) 64-Bit Server VM 1.8.0_171) started
2018-05-19 21:41:06:460 WARNING PredicateCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:491 INFO PredicateCPA:PredicateCPA.<init> Using predicate analysis with MathSAT5 version 5.5.0 (59014c8d54e1) (Dec 5 2017 11:43:02, gmp 6.1.0, gcc 4.8.5, 64-bit, reentrant).
2018-05-19 21:41:06:534 WARNING AssumptionStorageCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:587 WARNING ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:592 WARNING ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:703 WARNING InductionStepCase:PredicateCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:705 INFO InductionStepCase:PredicateCPA:PredicateCPA.<init> Using predicate analysis with MathSAT5 version 5.5.0 (59014c8d54e1) (Dec 5 2017 11:43:02, gmp 6.1.0, gcc 4.8.5, 64-bit, reentrant).
2018-05-19 21:41:06:709 WARNING InductionStepCase:AssumptionStorageCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:716 WARNING InductionStepCase:ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:718 WARNING InductionStepCase:ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:731 WARNING KInductionInvariantGenerator:PredicateCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:733 INFO KInductionInvariantGenerator:PredicateCPA:PredicateCPA.<init> Using predicate analysis with MathSAT5 version 5.5.0 (59014c8d54e1) (Dec 5 2017 11:43:02, gmp 6.1.0, gcc 4.8.5, 64-bit, reentrant).
2018-05-19 21:41:06:736 WARNING KInductionInvariantGenerator:AssumptionStorageCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:742 WARNING KInductionInvariantGenerator:ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:746 WARNING KInductionInvariantGenerator:ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:761 WARNING KInductionInvariantGenerator:InductionStepCase:PredicateCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:762 INFO KInductionInvariantGenerator:InductionStepCase:PredicateCPA:PredicateCPA.<init> Using predicate analysis with MathSAT5 version 5.5.0 (59014c8d54e1) (Dec 5 2017 11:43:02, gmp 6.1.0, gcc 4.8.5, 64-bit, reentrant).
2018-05-19 21:41:06:765 WARNING KInductionInvariantGenerator:InductionStepCase:AssumptionStorageCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:777 WARNING KInductionInvariantGenerator:InductionStepCase:ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:779 WARNING KInductionInvariantGenerator:InductionStepCase:ARGCPA:JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:789 WARNING JavaSMT:Mathsat5SolverContext.<init> MathSAT5 is available for research and evaluation purposes only. It can not be used in a commercial environment, particularly as part of a commercial product, without written permission. MathSAT5 is provided as is, without any warranty. Please write to mathsat@fbk.eu for additional questions regarding licensing MathSAT5 or obtaining more up-to-date versions.
2018-05-19 21:41:06:797 INFO CPAchecker.runAlgorithm Starting analysis ...
2018-05-19 21:41:06:823 INFO AbstractBMCAlgorithm.run Creating formula for program
2018-05-19 21:41:06:826 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.run Creating formula for program
2018-05-19 21:41:06:910 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2018-05-19 21:41:06:913 INFO AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2018-05-19 21:41:06:915 INFO AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2018-05-19 21:41:06:915 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2018-05-19 21:41:06:941 INFO KInductionProver.check Running algorithm to create induction hypothesis
2018-05-19 21:41:06:949 INFO KInductionInvariantGenerator:KInductionProver.check Running algorithm to create induction hypothesis
2018-05-19 21:41:06:989 INFO KInductionProver.check Starting induction check...
2018-05-19 21:41:06:992 INFO KInductionInvariantGenerator:KInductionProver.check Starting induction check...
2018-05-19 21:41:07:016 INFO LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState Adjusting maxLoopIterations to 2
2018-05-19 21:41:07:016 INFO AbstractBMCAlgorithm.run Creating formula for program
2018-05-19 21:41:07:037 INFO AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2018-05-19 21:41:07:037 INFO AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2018-05-19 21:41:07:044 INFO KInductionInvariantGenerator:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState Adjusting maxLoopIterations to 2
2018-05-19 21:41:07:044 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.run Creating formula for program
2018-05-19 21:41:07:050 INFO KInductionProver.check Running algorithm to create induction hypothesis
2018-05-19 21:41:07:067 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2018-05-19 21:41:07:068 INFO KInductionProver.check Starting induction check...
2018-05-19 21:41:07:068 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2018-05-19 21:41:07:076 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2018-05-19 21:41:07:081 INFO LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState Adjusting maxLoopIterations to 3
2018-05-19 21:41:07:081 INFO AbstractBMCAlgorithm.run Creating formula for program
2018-05-19 21:41:07:093 INFO AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2018-05-19 21:41:07:093 INFO AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2018-05-19 21:41:07:108 INFO KInductionProver.check Running algorithm to create induction hypothesis
2018-05-19 21:41:07:111 INFO KInductionInvariantGenerator:KInductionProver.check Running algorithm to create induction hypothesis
2018-05-19 21:41:07:120 INFO KInductionProver.check Starting induction check...
2018-05-19 21:41:07:124 INFO KInductionInvariantGenerator:KInductionProver.check Starting induction check...
2018-05-19 21:41:07:132 INFO KInductionInvariantGenerator:KInductionProver.check Running algorithm to create induction hypothesis
2018-05-19 21:41:07:135 INFO KInductionInvariantGenerator:KInductionProver.check Starting induction check...
2018-05-19 21:41:07:136 INFO LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState Adjusting maxLoopIterations to 4
2018-05-19 21:41:07:137 INFO AbstractBMCAlgorithm.run Creating formula for program
2018-05-19 21:41:07:149 INFO AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2018-05-19 21:41:07:150 INFO AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2018-05-19 21:41:07:161 INFO KInductionProver.check Running algorithm to create induction hypothesis
2018-05-19 21:41:07:175 INFO KInductionProver.check Starting induction check...
2018-05-19 21:41:07:191 INFO CPAchecker.runAlgorithm Stopping analysis ...
PredicateCPA statistics
-----------------------
Number of abstractions: 4 (4% of all post computations)
Times abstraction was reused: 0
Because of function entry/exit: 0 (0%)
Because of loop head: 0 (0%)
Because of join nodes: 0 (0%)
Because of threshold: 0 (0%)
Because of target state: 4 (100%)
Times precision was empty: 4 (100%)
Times precision was {false}: 0 (0%)
Times result was cached: 0 (0%)
Times cartesian abs was used: 0 (0%)
Times boolean abs was used: 0 (0%)
Times result was 'false': 0 (0%)
Number of strengthen sat checks: 0
Number of coverage checks: 0
BDD entailment checks: 0
Number of SMT sat checks: 0
trivial: 0
cached: 0
Max ABE block size: 25
Number of predicates discovered: 0
Time for post operator: 0.049s
Time for path formula creation: 0.049s
Time for strengthen operator: 0.003s
Time for prec operator: 0.002s
Time for abstraction: 0.000s (Max: 0.000s, Count: 4)
Solving time: 0.000s (Max: 0.000s)
Model enumeration time: 0.000s
Time for BDD construction: 0.000s (Max: 0.000s)
Time for merge operator: 0.000s
Time for coverage check: 0.000s
Total time for SMT solver (w/o itp): 0.000s
Total number of created targets for pointer analysis: 0
PrecisionBootstrap statistics
-----------------------------
Init. function predicates: 0
Init. global predicates: 0
Init. location predicates: 0
Invariant Generation statistics
-------------------------------
Bounds CPA statistics
---------------------
Bound k: 4
Maximum loop iteration reached: 5
ValueAnalysisCPA statistics
---------------------------
Number of variables per state: 0.85 (sum: 76, count: 89, min: 0, max: 2)
Number of global variables per state: 0.00 (sum: 0, count: 89, min: 0, max: 0)
Number of assumptions: 16
Number of deterministic assumptions: 0
Level of Determinism: 0%
ValueAnalysisPrecisionAdjustment statistics
-------------------------------------------
Number of abstraction computations: 95
Total time for liveness abstraction: 0.000s
Total time for abstraction computation: 0.001s
Total time for path thresholds: 0.000s
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.003s
Automaton transfers with branching: 0
Automaton transfer successors: 0.96 (sum: 95, count: 99, min: 0, max: 1) [0 x 4, 1 x 95]
CPA algorithm statistics
------------------------
Number of iterations: 99
Max size of waitlist: 3
Average size of waitlist: 1
LoopstackSortedWaitlist: 1.00 (sum: 286, count: 286, min: 0, max: 10)
ReversePostorderSortedWaitlist: 0.00 (sum: 0, count: 352, min: 0, max: 0)
LoopIterationSortedWaitlist: 0.77 (sum: 220, count: 286, min: 0, max: 7)
CallstackSortedWaitlist: 32.50 (sum: 130, count: 4, min: 13, max: 52)
Number of computed successors: 95
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 0
Number of times breaked: 0
Total time for CPA algorithm: 0.130s (Max: 0.086s)
Time for choose from waitlist: 0.001s
Time for precision adjustment: 0.022s
Time for transfer relation: 0.096s
Time for stop operator: 0.004s
Time for adding to reached set: 0.003s
BMC algorithm statistics
------------------------
Time for BMC formula creation: 0.131s
Time for final sat check: 0.001s
Time for bounding assertions check: 0.004s
Time for induction formula creation: 0.089s
Time for induction check: 0.068s
CPA algorithm statistics
------------------------
Number of iterations: 55
Max size of waitlist: 3
Average size of waitlist: 1
LoopstackSortedWaitlist: 0.90 (sum: 52, count: 58, min: 0, max: 10)
ReversePostorderSortedWaitlist: 0.00 (sum: 0, count: 70, min: 0, max: 0)
LoopIterationSortedWaitlist: 0.69 (sum: 40, count: 58, min: 0, max: 7)
CallstackSortedWaitlist: 19.50 (sum: 39, count: 2, min: 13, max: 26)
Number of computed successors: 53
Max successors for one state: 2
Number of times merged: 0
Number of times stopped: 0
Number of times breaked: 0
Total time for CPA algorithm: 0.094s (Max: 0.080s)
Time for choose from waitlist: 0.001s
Time for precision adjustment: 0.013s
Time for transfer relation: 0.076s
Time for stop operator: 0.000s
Time for adding to reached set: 0.000s
k-Induction-based invariant generator statistics
------------------------------------------------
Time for invariant generation: 0.343s
Total number of candidates: 0
Number of confirmed candidates: 1
Time for BMC formula creation: 0.103s
Time for final sat check: 0.009s
Time for bounding assertions check: 0.010s
Time for induction formula creation: 0.057s
Time for induction check: 0.064s
k-Induction-based invariant generator statistics
------------------------------------------------
Time for invariant generation: 0.343s
Total number of candidates: 0
Number of confirmed candidates: 1
Time for BMC formula creation: 0.103s
Time for final sat check: 0.009s
Time for bounding assertions check: 0.010s
Time for induction formula creation: 0.057s
Time for induction check: 0.064s
Code Coverage
-----------------------------
Function coverage: 1.000
Visited lines: 13
Total lines: 13
Line coverage: 1.000
Visited conditions: 4
Total conditions: 4
Condition coverage: 1.000
CPAchecker general statistics
-----------------------------
Number of program locations: 32
Number of CFA edges (per node): 33 (count: 32, min: 0, max: 2, avg: 1.03)
Number of relevant variables: 6
Number of functions: 2
Number of loops (and loop nodes): 1 (sum: 10, min: 10, max: 10, avg: 10.00)
Size of reached set: 89
Number of reached locations: 31 (97%)
Avg states per location: 2
Max states per location: 5 (at node N16)
Number of reached functions: 2 (100%)
Number of partitions: 89
Avg size of partitions: 1
Max size of partitions: 1
Number of target states: 0
Time for analysis setup: 1.208s
Time for loading CPAs: 0.377s
Time for loading parser: 0.221s
Time for CFA construction: 0.404s
Time for parsing file(s): 0.228s
Time for AST to CFA: 0.077s
Time for CFA sanity check: 0.005s
Time for post-processing: 0.063s
Time for CFA export: 0.448s
Time for function pointers resolving: 0.001s
Function calls via function pointers: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Instrumented function pointer calls: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Function calls with function pointer arguments: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Instrumented function pointer arguments: 0 (count: 1, min: 0, max: 0, avg: 0.00)
Time for var class.: 0.033s
Time for collecting variables: 0.011s
Time for solving dependencies: 0.001s
Time for building hierarchy: 0.000s
Time for building classification: 0.020s
Time for exporting data: 0.001s
Time for Analysis: 0.393s
CPU time for analysis: 1.270s
Time for analyzing result: 0.001s
Total time for CPAchecker: 1.605s
Total CPU time for CPAchecker: 4.720s
Time for statistics: 0.203s
Time for Garbage Collector: 0.053s (in 4 runs)
Garbage Collector(s) used: PS MarkSweep, PS Scavenge
Used heap memory: 80MB ( 76 MiB) max; 46MB ( 44 MiB) avg; 93MB ( 89 MiB) peak
Used non-heap memory: 39MB ( 38 MiB) max; 27MB ( 26 MiB) avg; 44MB ( 42 MiB) peak
Used in PS Old Gen pool: 17MB ( 16 MiB) max; 8MB ( 8 MiB) avg; 17MB ( 16 MiB) peak
Allocated heap memory: 251MB ( 240 MiB) max; 229MB ( 218 MiB) avg
Allocated non-heap memory: 41MB ( 39 MiB) max; 28MB ( 27 MiB) avg
Total process virtual memory: 4053MB ( 3866 MiB) max; 3929MB ( 3747 MiB) avg
analysis.algorithm.BMC = true
analysis.entryFunction = main
analysis.programNames = eq2.c
analysis.traversal.order = bfs
analysis.traversal.useCallstack = true
analysis.traversal.useReverseLoopIterationCount = true
analysis.traversal.useReverseLoopstack = true
analysis.traversal.useReversePostorder = true
ARGCPA.cpa = cpa.composite.CompositeCPA
bmc.induction = true
bmc.invariantGenerationStrategy = INDUCTION
bmc.invariantGeneratorConfig = kiki/pdr.properties
CompositeCPA.cpas = cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.predicate.PredicateCPA, cpa.assumptions.storage.AssumptionStorageCPA, cpa.loopbound.LoopBoundCPA, cpa.value.ValueAnalysisCPA, cpa.pointer2.PointerCPA, cpa.input.InputCPA
cpa = cpa.arg.ARGCPA
cpa.arg.compressWitness = false
cpa.arg.proofWitness = proofWitness.graphml
cpa.automaton.breakOnTargetState = 0
cpa.callstack.depth = 1
cpa.loopbound.maxLoopIterationAdjusterFactory = INCREMENT
cpa.loopbound.maxLoopIterations = 1
cpa.loopbound.maxLoopIterationsUpperBound = 0
cpa.predicate.blk.alwaysAtFunctions = false
cpa.predicate.blk.alwaysAtLoops = false
cpa.predicate.blk.useCache = false
cpa.predicate.invariants.export = false
cpa.predicate.invariants.exportAsPrecision = false
cpa.predicate.predmap.export = false
cpa.value.merge = JOIN
log.level = INFO
report.witness = true
specification = config/specification/sv-comp-reachability.spc