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_int(); |
9 | |
10 | int main(void) { |
11 | unsigned int x = 0; |
12 | while (__VERIFIER_nondet_int()) { |
13 | x += 4; |
14 | } |
15 | __VERIFIER_assert(!(x%4)); |
16 | return 0; |
17 | } |
2019-02-27 13:03:30:418 INFO CPAchecker.run CPAchecker 1.7-svn 28007 (OpenJDK 64-Bit Server VM 1.8.0_191) started
2019-02-27 13:03:31:091 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.
2019-02-27 13:03:31:123 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).
2019-02-27 13:03:31:151 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.
2019-02-27 13:03:31:188 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.
2019-02-27 13:03:31:198 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.
2019-02-27 13:03:31:276 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.
2019-02-27 13:03:31:278 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).
2019-02-27 13:03:31:285 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.
2019-02-27 13:03:31:296 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.
2019-02-27 13:03:31:300 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.
2019-02-27 13:03:31:327 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.
2019-02-27 13:03:31:328 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).
2019-02-27 13:03:31:337 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.
2019-02-27 13:03:31:355 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.
2019-02-27 13:03:31:360 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.
2019-02-27 13:03:31:385 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.
2019-02-27 13:03:31:386 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).
2019-02-27 13:03:31:397 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.
2019-02-27 13:03:31:406 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.
2019-02-27 13:03:31:413 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.
2019-02-27 13:03:31:440 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.
2019-02-27 13:03:31:447 INFO CPAchecker.runAlgorithm Starting analysis ...
2019-02-27 13:03:31:468 INFO AbstractBMCAlgorithm.run Creating formula for program
2019-02-27 13:03:31:469 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.run Creating formula for program
2019-02-27 13:03:31:523 INFO AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2019-02-27 13:03:31:523 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2019-02-27 13:03:31:528 INFO AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2019-02-27 13:03:31:528 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2019-02-27 13:03:31:552 INFO KInductionInvariantGenerator:KInductionProver.check Running algorithm to create induction hypothesis
2019-02-27 13:03:31:554 INFO KInductionProver.check Running algorithm to create induction hypothesis
2019-02-27 13:03:31:587 INFO KInductionProver.check Starting induction check...
2019-02-27 13:03:31:587 INFO KInductionInvariantGenerator:KInductionProver.check Starting induction check...
2019-02-27 13:03:31:607 INFO LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState Adjusting maxLoopIterations to 2
2019-02-27 13:03:31:608 INFO AbstractBMCAlgorithm.run Creating formula for program
2019-02-27 13:03:31:622 INFO KInductionInvariantGenerator:LoopBoundCPA:LoopBoundPrecisionAdjustment.nextState Adjusting maxLoopIterations to 2
2019-02-27 13:03:31:622 INFO AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2019-02-27 13:03:31:622 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.run Creating formula for program
2019-02-27 13:03:31:622 INFO AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2019-02-27 13:03:31:634 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2019-02-27 13:03:31:634 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2019-02-27 13:03:31:638 INFO KInductionInvariantGenerator:AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2019-02-27 13:03:31:643 INFO KInductionProver.check Running algorithm to create induction hypothesis
2019-02-27 13:03:31:655 INFO KInductionInvariantGenerator:KInductionProver.check Running algorithm to create induction hypothesis
2019-02-27 13:03:31:668 INFO KInductionProver.check Starting induction check...
2019-02-27 13:03:31:670 INFO KInductionInvariantGenerator:KInductionProver.check Starting induction check...
2019-02-27 13:03:31:681 INFO KInductionInvariantGenerator:KInductionProver.check Running algorithm to create induction hypothesis
2019-02-27 13:03:31:684 INFO KInductionInvariantGenerator:KInductionProver.check Starting induction check...
2019-02-27 13:03:31:690 INFO CPAchecker.runAlgorithm Stopping analysis ...
PredicateCPA statistics
-----------------------
Number of abstractions: 0 (0% of all post computations)
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: 0
Number of predicates discovered: 0
Time for post operator: 0.021s
Time for path formula creation: 0.021s
Time for strengthen operator: 0.002s
Time for prec operator: 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: 2
Maximum loop iteration reached: 3
ValueAnalysisCPA statistics
---------------------------
Number of variables per state: 1.52 (sum: 50, count: 33, min: 0, max: 3)
Number of global variables per state: 0.00 (sum: 0, count: 33, min: 0, max: 0)
Number of assumptions: 12
Number of deterministic assumptions: 0
Level of Determinism: 0%
ValueAnalysisPrecisionAdjustment statistics
-------------------------------------------
Number of abstraction computations: 33
Total time for liveness abstraction: 0.000s
Total time for abstraction computation: 0.000s
Total time for path thresholds: 0.000s
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.000s
Automaton transfers with branching: 0
Automaton transfer successors: 1.00 (sum: 33, count: 33, min: 1, max: 1) [1 x 33]
CPA algorithm statistics
------------------------
Number of iterations: 35
Max size of waitlist: 2
Average size of waitlist: 1
LoopstackSortedWaitlist: 0.40 (sum: 20, count: 50, min: 0, max: 5)
ReversePostorderSortedWaitlist: 0.00 (sum: 0, count: 62, min: 0, max: 0)
LoopIterationSortedWaitlist: 0.16 (sum: 8, count: 50, min: 0, max: 2)
CallstackSortedWaitlist: 7.50 (sum: 15, count: 2, min: 5, max: 10)
Number of computed successors: 33
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.066s (Max: 0.054s)
Time for choose from waitlist: 0.002s
Time for precision adjustment: 0.007s
Time for transfer relation: 0.052s
Time for stop operator: 0.001s
Time for adding to reached set: 0.002s
BMC algorithm statistics
------------------------
Time for BMC formula creation: 0.068s
Time for final sat check: 0.004s
Time for bounding assertions check: 0.002s
Time for induction formula creation: 0.057s
Time for induction check: 0.039s
CPA algorithm statistics
------------------------
Number of iterations: 35
Max size of waitlist: 2
Average size of waitlist: 1
LoopstackSortedWaitlist: 0.40 (sum: 20, count: 50, min: 0, max: 5)
ReversePostorderSortedWaitlist: 0.00 (sum: 0, count: 62, min: 0, max: 0)
LoopIterationSortedWaitlist: 0.16 (sum: 8, count: 50, min: 0, max: 2)
CallstackSortedWaitlist: 7.50 (sum: 15, count: 2, min: 5, max: 10)
Number of computed successors: 33
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.063s (Max: 0.052s)
Time for choose from waitlist: 0.001s
Time for precision adjustment: 0.010s
Time for transfer relation: 0.049s
Time for stop operator: 0.000s
Time for adding to reached set: 0.003s
k-Induction-based invariant generator statistics
------------------------------------------------
Time for invariant generation: 0.229s
Total number of candidates: 0
Number of confirmed candidates: 1
Time for BMC formula creation: 0.064s
Time for final sat check: 0.007s
Time for bounding assertions check: 0.004s
Time for induction formula creation: 0.051s
Time for induction check: 0.177s
k-Induction-based invariant generator statistics
------------------------------------------------
Time for invariant generation: 0.229s
Total number of candidates: 0
Number of confirmed candidates: 1
Time for BMC formula creation: 0.064s
Time for final sat check: 0.007s
Time for bounding assertions check: 0.004s
Time for induction formula creation: 0.051s
Time for induction check: 0.178s
Code Coverage
-----------------------------
Function coverage: 1.000
Visited lines: 8
Total lines: 9
Line coverage: 0.889
Visited conditions: 3
Total conditions: 4
Condition coverage: 0.750
CPAchecker general statistics
-----------------------------
Number of program locations: 23
Number of CFA edges (per node): 24 (count: 23, min: 0, max: 2, avg: 1.04)
Number of relevant variables: 3
Number of functions: 2
Number of loops (and loop nodes): 1 (sum: 5, min: 5, max: 5, avg: 5.00)
Size of reached set: 33
Number of reached locations: 20 (87%)
Avg states per location: 1
Max states per location: 3 (at node N12)
Number of reached functions: 2 (100%)
Number of partitions: 33
Avg size of partitions: 1
Max size of partitions: 1
Number of target states: 0
Time for analysis setup: 1.013s
Time for loading CPAs: 0.319s
Time for loading parser: 0.151s
Time for CFA construction: 0.296s
Time for parsing file(s): 0.163s
Time for AST to CFA: 0.056s
Time for CFA sanity check: 0.005s
Time for post-processing: 0.050s
Time for CFA export: 0.421s
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.027s
Time for collecting variables: 0.009s
Time for solving dependencies: 0.001s
Time for building hierarchy: 0.000s
Time for building classification: 0.016s
Time for exporting data: 0.001s
Time for Analysis: 0.240s
CPU time for analysis: 0.640s
Time for analyzing result: 0.001s
Total time for CPAchecker: 1.258s
Total CPU time for CPAchecker: 3.410s
Time for statistics: 0.138s
Time for Garbage Collector: 0.040s (in 3 runs)
Garbage Collector(s) used: PS MarkSweep, PS Scavenge
Used heap memory: 124MB ( 118 MiB) max; 68MB ( 65 MiB) avg; 166MB ( 158 MiB) peak
Used non-heap memory: 39MB ( 37 MiB) max; 28MB ( 26 MiB) avg; 43MB ( 41 MiB) peak
Used in PS Old Gen pool: 14MB ( 13 MiB) max; 7MB ( 7 MiB) avg; 14MB ( 13 MiB) peak
Allocated heap memory: 504MB ( 481 MiB) max; 405MB ( 387 MiB) avg
Allocated non-heap memory: 40MB ( 38 MiB) max; 29MB ( 27 MiB) avg
Total process virtual memory: 4053MB ( 3866 MiB) max; 3915MB ( 3733 MiB) avg
analysis.algorithm.BMC = true
analysis.programNames = mod4.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
specification = config/specification/sv-comp-reachability.spc