% bin/jahob.opt -verbose Nat.java -nobackground -usedp cvcl
     _       _           _                  _____
    | | __ _| |__   ___ | |__              /     \
 _  | |/ _` | '_ \ / _ \| '_ \       x <==|  (J)  |===.
| |_| | (_| | | | | (_) | |_) |     ======+=======+==="  F
 \____/\__,_|_| |_|\___/|_.__/             \_____/  


Analyzing class Nat.
Checking initial state of class Nat
opening lemma file : Nat_INIT-lemmas.thy
No lemma file Nat_INIT-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file Nat_INIT-lemmas.thy.
Generated 0 proof obligations.
Checking rep of class Nat
opening lemma file : Nat_REP-lemmas.thy
No lemma file Nat_REP-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file Nat_REP-lemmas.thy.
Generated 0 proof obligations.

Now analyzing: ==== Procedure Nat.comm ====
Generating VCs...
Using direct VC generation.
Done generating VCs.
Processing VCs...opening lemma file : comm_Nat-lemmas.thy
No lemma file comm_Nat-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file comm_Nat-lemmas.thy.
Generated 1 proof obligations.

Proof obligation: (True ==>
    (((intplus (a :: int) (b :: int)) :: int) = ((intplus (b :: int) (a :: int)) :: int)))
.Running Built-in validity checker (after splitting)... Built-in validity checker (after splitting) failed to prove formula.
Running CVC Lite... CVC Lite proved formula.

======================================================================
CVC Lite proved 1 out of 1 sequents. Total time : 2.2 s
======================================================================
A total of 1 sequents out of 1 proved.

Done analyzing Procedure Nat.comm.

Now analyzing: ==== Procedure Nat.assoc ====
Generating VCs...
Using direct VC generation.
Done generating VCs.
Processing VCs...opening lemma file : assoc_Nat-lemmas.thy
No lemma file assoc_Nat-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file assoc_Nat-lemmas.thy.
Generated 1 proof obligations.

Proof obligation: (True ==>
    (((intplus (a :: int) (intplus (b :: int) (c :: int))) :: int) = ((intplus (intplus (a :: int) (b :: int)) (c :: int)) :: int)))
.Running Built-in validity checker (after splitting)... Built-in validity checker (after splitting) failed to prove formula.
Running CVC Lite... CVC Lite proved formula.

======================================================================
CVC Lite proved 1 out of 1 sequents. Total time : 0.3 s
======================================================================
A total of 1 sequents out of 1 proved.

Done analyzing Procedure Nat.assoc.

Now analyzing: ==== Procedure Nat.dist ====
Generating VCs...
Using direct VC generation.
Done generating VCs.
Processing VCs...opening lemma file : dist_Nat-lemmas.thy
No lemma file dist_Nat-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file dist_Nat-lemmas.thy.
Generated 1 proof obligations.

Proof obligation: (True ==>
    (((inttimes (a :: int) (intplus (b :: int) (c :: int))) :: int) = ((intplus (inttimes (a :: int) (b :: int)) (inttimes (a :: int) (c :: int))) :: int)))
.Running Built-in validity checker (after splitting)... Built-in validity checker (after splitting) failed to prove formula.
Running CVC Lite... CVC Lite proved formula.

======================================================================
CVC Lite proved 1 out of 1 sequents. Total time : 0.5 s
======================================================================
A total of 1 sequents out of 1 proved.

Done analyzing Procedure Nat.dist.

Now analyzing: ==== Procedure Nat.sum ====
Generating VCs...
Using direct VC generation.
Done generating VCs.
Processing VCs...opening lemma file : sum_Nat-lemmas.thy
No lemma file sum_Nat-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file sum_Nat-lemmas.thy.
Generated 1 proof obligations.

Proof obligation: (((0 :: int) <= (n :: int)) ==>
    comment ''InvHoldsInitially'' (((intplus (0 :: int) (0 :: int)) :: int) = ((inttimes (0 :: int) ((intplus (0 :: int) (1 :: int)) div (2 :: int))) :: int)))
.Running Built-in validity checker (after splitting)... Built-in validity checker (after splitting) failed to prove formula.
Running CVC Lite... CVC Lite proved formula.

Proof obligation: ([|((0 :: int) <= (n :: int));
(((intplus (s_11 :: int) (i_9 :: int)) :: int) = ((inttimes (i_9 :: int) ((intplus (i_9 :: int) (1 :: int)) div (2 :: int))) :: int));
(((i_9 :: int) ~= ((intplus (n :: int) (1 :: int)) :: int)) :: bool)|] ==>
    comment ''InvPreservation'' (((intplus ((intplus (s_11 :: int) (i_9 :: int)) :: int) ((intplus (i_9 :: int) (1 :: int)) :: int)) :: int) = ((inttimes ((intplus (i_9 :: int) (1 :: int)) :: int) ((intplus ((intplus (i_9 :: int) (1 :: int)) :: int) (1 :: int)) div (2 :: int))) :: int)))
.Running Built-in validity checker (after splitting)... Built-in validity checker (after splitting) failed to prove formula.
Running CVC Lite... CVC Lite proved formula.

Proof obligation: ([|((0 :: int) <= (n :: int));
(((intplus (s_11 :: int) (i_9 :: int)) :: int) = ((inttimes (i_9 :: int) ((intplus (i_9 :: int) (1 :: int)) div (2 :: int))) :: int));
(~(((i_9 :: int) ~= ((intplus (n :: int) (1 :: int)) :: int)) :: bool))|] ==>
    comment ''ReturnStatement'' ((s_11 :: int) = ((inttimes (n :: int) ((intplus (n :: int) (1 :: int)) div (2 :: int))) :: int)))
.Running Built-in validity checker (after splitting)... Built-in validity checker (after splitting) failed to prove formula.
Running CVC Lite... CVC Lite proved formula.

======================================================================
CVC Lite proved 3 out of 3 sequents. Total time : 0.9 s
======================================================================
A total of 3 sequents out of 3 proved.

Done analyzing Procedure Nat.sum.

Analyzing class Array.
Checking initial state of class Array
opening lemma file : Array_INIT-lemmas.thy
No lemma file Array_INIT-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file Array_INIT-lemmas.thy.
Generated 1 proof obligations.
Trivially true.
eProved during splitting: ([|(ALL (this::obj). (((Array_length this) :: int) = (0 :: int)));
(Array_hidden = {});
((Object_alloc :: obj set) = ({null} :: obj set))|] ==>
    (ALL (this::obj). (((Array_length this) :: int) = (0 :: int))))

======================================================================
Built-in validity checker proved 1 sequents during splitting.
======================================================================
A total of 1 sequents out of 1 proved.
Checking rep of class Array
opening lemma file : Array_REP-lemmas.thy
No lemma file Array_REP-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file Array_REP-lemmas.thy.
Generated 0 proof obligations.

Analyzing class Object.
Checking initial state of class Object
opening lemma file : Object_INIT-lemmas.thy
No lemma file Object_INIT-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file Object_INIT-lemmas.thy.
Generated 0 proof obligations.
Checking rep of class Object
opening lemma file : Object_REP-lemmas.thy
No lemma file Object_REP-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file Object_REP-lemmas.thy.
Generated 0 proof obligations.

Now analyzing: ==== Procedure Object.hashCode ====
Generating VCs...
Using direct VC generation.
Done generating VCs.
Processing VCs...opening lemma file : hashCode_Object-lemmas.thy
No lemma file hashCode_Object-lemmas.thyEnd of file while searching for lemma keyword at position 0.
Retrieved 0 lemmas from lemma file hashCode_Object-lemmas.thy.
Generated 1 proof obligations.
eProved during splitting: (True --> True)

======================================================================
Built-in validity checker proved 1 sequents during splitting.
======================================================================
A total of 1 sequents out of 1 proved.

Done analyzing Procedure Object.hashCode.

0=== Verification SUCCEEDED.