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 += 2; |
14 | } |
15 | __VERIFIER_assert(!(x%2)); |
16 | return 0; |
17 | } |
2018-05-19 20:19:07:247 INFO CPAchecker.run CPAchecker 1.7-svn (Java HotSpot(TM) 64-Bit Server VM 1.8.0_171) started
2018-05-19 20:19:08:094 WARNING CPAchecker.printConfigurationWarnings The following configuration options were specified but are not used:
cpa.invariants.interestingVariableLimit
cpa.arg.compressWitness
cpa.invariants.abstractionStateFactory
cpa.invariants.maximumFormulaDepth
cpa.arg.proofWitness
cpa.invariants.useMod2Template
2018-05-19 20:19:08:094 INFO CPAchecker.runAlgorithm Starting analysis ...
2018-05-19 20:19:08:218 WARNING Parallel analysis 1: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 20:19:08:224 WARNING Parallel analysis 2: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 20:19:08:257 INFO Parallel analysis 1: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 20:19:08:261 WARNING Parallel analysis 2: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 20:19:08:291 WARNING Parallel analysis 1: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 20:19:08:344 WARNING Parallel analysis 1: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 20:19:08:346 WARNING Parallel analysis 1: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 20:19:08:430 WARNING Parallel analysis 1: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 20:19:08:431 INFO Parallel analysis 1: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 20:19:08:435 WARNING Parallel analysis 1: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 20:19:08:447 WARNING Parallel analysis 1: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 20:19:08:456 WARNING Parallel analysis 1: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 20:19:08:465 WARNING Parallel analysis 1: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 20:19:08:486 INFO Parallel analysis 1:AbstractBMCAlgorithm.run Creating formula for program
2018-05-19 20:19:08:502 INFO Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions Adjusting interestingVariableLimit to 1
2018-05-19 20:19:08:502 INFO Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@4c771e7
2018-05-19 20:19:08:503 INFO Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis Updating reached set provided to other analyses
2018-05-19 20:19:08:541 INFO Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions Adjusting interestingVariableLimit to 2
2018-05-19 20:19:08:541 INFO Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@4c771e7
2018-05-19 20:19:08:542 INFO Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis Updating reached set provided to other analyses
2018-05-19 20:19:08:570 INFO Parallel analysis 1:AbstractBMCAlgorithm.boundedModelCheck Starting satisfiability check...
2018-05-19 20:19:08:574 INFO Parallel analysis 1:AbstractBMCAlgorithm.checkBoundingAssertions Starting assertions check...
2018-05-19 20:19:08:592 INFO Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions Adjusting interestingVariableLimit to 3
2018-05-19 20:19:08:592 INFO Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@4c771e7
2018-05-19 20:19:08:592 INFO Parallel analysis 1:KInductionProver.check Running algorithm to create induction hypothesis
2018-05-19 20:19:08:593 INFO Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis Updating reached set provided to other analyses
2018-05-19 20:19:08:658 INFO Parallel analysis 1:KInductionProver.check Starting induction check...
2018-05-19 20:19:08:661 INFO Parallel analysis 2:InvariantsCPA:InvariantsCPA$InterestingVariableLimitAdjuster.adjustConditions Adjusting interestingVariableLimit to 4
2018-05-19 20:19:08:661 INFO Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis Adjusting precision for CPA org.sosy_lab.cpachecker.cpa.invariants.InvariantsCPA@4c771e7
2018-05-19 20:19:08:662 INFO Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis Updating reached set provided to other analyses
2018-05-19 20:19:08:674 INFO ParallelAlgorithm.handleFutureResults config/components/kInduction/kInduction.properties finished successfully.
2018-05-19 20:19:08:681 INFO Parallel analysis 2:ParallelAlgorithm.runParallelAnalysis Analysis was terminated
2018-05-19 20:19:08:681 INFO CPAchecker.runAlgorithm Stopping analysis ...
Parallel Algorithm statistics
-----------------------------
Number of algorithms used: 2
Successful analysis: config/components/kInduction/kInduction.properties
Statistics for: config/components/kInduction/kInduction.properties
==================================================================
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.032s
Time for path formula creation: 0.032s
Time for strengthen operator: 0.000s
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: 1
Maximum loop iteration reached: 2
ValueAnalysisCPA statistics
---------------------------
Number of variables per state: 1.24 (sum: 26, count: 21, min: 0, max: 3)
Number of global variables per state: 0.00 (sum: 0, count: 21, min: 0, max: 0)
Number of assumptions: 6
Number of deterministic assumptions: 0
Level of Determinism: 0%
ValueAnalysisPrecisionAdjustment statistics
-------------------------------------------
Number of abstraction computations: 20
Total time for liveness abstraction: 0.000s
Total time for abstraction computation: 0.002s
Total time for path thresholds: 0.000s
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.001s
Automaton transfers with branching: 0
Automaton transfer successors: 1.00 (sum: 20, count: 20, min: 1, max: 1) [1 x 20]
CPA algorithm statistics
------------------------
Number of iterations: 21
Max size of waitlist: 2
Average size of waitlist: 1
LoopstackSortedWaitlist: 0.31 (sum: 5, count: 16, min: 0, max: 5)
ReversePostorderSortedWaitlist: 0.00 (sum: 0, count: 19, min: 0, max: 0)
LoopIterationSortedWaitlist: 0.13 (sum: 2, count: 16, min: 0, max: 2)
CallstackSortedWaitlist: 5.00 (sum: 5, count: 1, min: 5, max: 5)
Number of computed successors: 20
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.080s (Max: 0.080s)
Time for choose from waitlist: 0.001s
Time for precision adjustment: 0.007s
Time for transfer relation: 0.071s
Time for stop operator: 0.000s
Time for adding to reached set: 0.000s
BMC algorithm statistics
------------------------
Time for BMC formula creation: 0.081s
Time for final sat check: 0.004s
Time for bounding assertions check: 0.001s
Time for induction formula creation: 0.064s
Time for induction check: 0.014s
Statistics for: config/components/invariantGeneration-no-out.properties
=======================================================================
AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Number of states: 1
Total time for successor computation: 0.005s
Automaton transfers with branching: 0
Automaton transfer successors: 0.97 (sum: 136, count: 140, min: 0, max: 1) [0 x 4, 1 x 136]
CPA algorithm statistics
------------------------
Number of iterations: 128
Max size of waitlist: 2
Average size of waitlist: 1
ReversePostorderSortedWaitlist: 0.00 (sum: 0, count: 4, min: 0, max: 0)
Number of computed successors: 136
Max successors for one state: 2
Number of times merged: 42
Number of times stopped: 46
Number of times breaked: 0
Total time for CPA algorithm: 0.259s (Max: 0.125s)
Time for choose from waitlist: 0.002s
Time for precision adjustment: 0.003s
Time for transfer relation: 0.155s
Time for merge operator: 0.071s
Time for stop operator: 0.024s
Time for adding to reached set: 0.000s
Other statistics
================
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: 21
Number of reached locations: 20 (87%)
Avg states per location: 1
Max states per location: 2 (at node N12)
Number of reached functions: 2 (100%)
Number of partitions: 21
Avg size of partitions: 1
Max size of partitions: 1
Number of target states: 0
Time for analysis setup: 0.833s
Time for loading CPAs: 0.155s
Time for loading parser: 0.228s
Time for CFA construction: 0.424s
Time for parsing file(s): 0.238s
Time for AST to CFA: 0.089s
Time for CFA sanity check: 0.005s
Time for post-processing: 0.063s
Time for CFA export: 0.521s
Time for function pointers resolving: 0.002s
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.032s
Time for collecting variables: 0.010s
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.586s
CPU time for analysis: 2.060s
Time for analyzing result: 0.000s
Total time for CPAchecker: 1.423s
Total CPU time for CPAchecker: 4.230s
Time for statistics: 0.215s
Time for Garbage Collector: 0.060s (in 4 runs)
Garbage Collector(s) used: PS MarkSweep, PS Scavenge
Used heap memory: 80MB ( 76 MiB) max; 45MB ( 43 MiB) avg; 93MB ( 89 MiB) peak
Used non-heap memory: 38MB ( 37 MiB) max; 26MB ( 24 MiB) avg; 44MB ( 42 MiB) peak
Used in PS Old Gen pool: 17MB ( 16 MiB) max; 7MB ( 7 MiB) avg; 17MB ( 16 MiB) peak
Allocated heap memory: 251MB ( 240 MiB) max; 232MB ( 221 MiB) avg
Allocated non-heap memory: 40MB ( 38 MiB) max; 27MB ( 25 MiB) avg
Total process virtual memory: 4190MB ( 3996 MiB) max; 3960MB ( 3776 MiB) avg
analysis.entryFunction = main
analysis.programNames = even.c
analysis.useParallelAnalyses = true
cpa.arg.compressWitness = false
cpa.arg.proofWitness = proofWitness.graphml
cpa.invariants.abstractionStateFactory = ENTERING_EDGES
cpa.invariants.interestingVariableLimit = 0
cpa.invariants.maximumFormulaDepth = 1
cpa.invariants.useMod2Template = true
log.level = INFO
parallelAlgorithm.configFiles = components/kInduction/kInduction.properties, components/invariantGeneration-no-out.properties::supply-reached-refinable
report.witness = true
specification = config/specification/sv-comp-reachability.spc