Commit b6164aa2 authored by MARCHE Claude's avatar MARCHE Claude

jessie3: upgrade to CVC4 1.4

parent 8e850a73
......@@ -64,7 +64,7 @@ let process () =
[ "Z431", "Z3,4.3.1";
"Z32 ", "Z3,3.2";
"C241", "CVC3,2.4.1";
"C413", "CVC4,1.3";
"C414", "CVC4,1.4";
"A952", "Alt-Ergo,0.95.2,";
]
with e ->
......
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] preprocessing with "gcc -C -E -I. tests/basic/constants.c"
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] found 5 logic decl(s)
[jessie3] made 1 theory(ies)
[jessie3] made 0 function(s)
[jessie3] Running provers...
[jessie3] running theory 1:
[jessie3] theory Global_logic_declarations
(* use why3.BuiltIn *)
(* use why3.BuiltIn.BuiltIn *)
(* use int.Int *)
......@@ -22,21 +29,21 @@
lemma test4 : 0x1.1p4 = 17.0
end
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (test1): Valid, Valid, Valid, Valid
[jessie3] Task 2 (test_ofl): Valid, Valid, Valid, Valid
[jessie3] Task 3 (test2): Valid, Valid, Valid, Valid
[jessie3] Task 4 (test3): Valid, Valid, Valid, Valid
[jessie3] Task 5 (test4): Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (test1): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2 (test_ofl): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 3 (test2): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 4 (test3): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 5 (test4): Valid, Valid, Valid, Valid, Valid
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
(* use why3.BuiltIn.BuiltIn *)
(* use why3.Bool *)
(* use why3.Bool.Bool *)
(* use why3.Unit *)
(* use why3.Unit.Unit *)
(* use why3.Prelude *)
(* use why3.Prelude.Prelude *)
(* use int.Int *)
......@@ -48,6 +55,6 @@
(* use ref.Ref *)
(* use mach_int.Int32 *)
(* use mach.int.Int32 *)
end
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] preprocessing with "gcc -C -E -I. tests/basic/forty-two.c"
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] processing function f
[jessie3] created program function f (738)
[jessie3] created program function f (757)
[jessie3] processing function g
[jessie3] created program function g (740)
[jessie3] created program function g (759)
[jessie3] found 0 logic decl(s)
[jessie3] made 0 theory(ies)
[jessie3] made 2 function(s)
[jessie3] Running provers...
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
(* use why3.BuiltIn.BuiltIn *)
(* use why3.Bool *)
(* use why3.Bool.Bool *)
(* use why3.Unit *)
(* use why3.Unit.Unit *)
(* use why3.Prelude *)
(* use why3.Prelude.Prelude *)
(* use int.Int *)
......@@ -24,7 +31,7 @@
(* use ref.Ref *)
(* use mach_int.Int32 *)
(* use mach.int.Int32 *)
goal WP_parameter_f : (6 * 7) = 42
......@@ -44,6 +51,6 @@
(forall us_retres:int32.
us_retres = o3 -> to_int us_retres = 42)))))
end
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter g): Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter g): Valid, Unknown, Valid, Valid, Valid
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] preprocessing with "gcc -C -E -I. tests/basic/incr.c"
[jessie3] Loading prover drivers...
[jessie3] Translating to Why3...
[jessie3] processing function f
[jessie3] created program function f (738)
[jessie3] created program function f (757)
[jessie3] processing function h
[jessie3] created program function h (744)
[jessie3] created program function h (763)
[jessie3] found 0 logic decl(s)
[jessie3] made 0 theory(ies)
[jessie3] made 3 function(s)
[jessie3] Running provers...
[jessie3] running theory 1:
[jessie3] theory C_Functions
(* use why3.BuiltIn *)
(* use why3.BuiltIn.BuiltIn *)
(* use why3.Bool *)
(* use why3.Bool.Bool *)
(* use why3.Unit *)
(* use why3.Unit.Unit *)
(* use why3.Prelude *)
(* use why3.Prelude.Prelude *)
(* use int.Int *)
......@@ -24,7 +31,7 @@
(* use ref.Ref *)
(* use mach_int.Int32 *)
(* use mach.int.Int32 *)
goal WP_parameter_f :
forall x:int32.
......@@ -51,6 +58,6 @@
to_int o = (to_int g + to_int x) ->
(forall g1:int32. g1 = o -> to_int g1 = (to_int g + to_int x)))
end
[jessie3] Provers: Alt-Ergo 0.95.1, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter h): Valid, Valid, Valid, Valid
[jessie3] Provers: Alt-Ergo 0.95.2, CVC4 1.4, CVC3 2.4.1, Z3 3.2, Z3 4.3.1
[jessie3] Task 1 (WP_parameter f): Valid, Valid, Valid, Valid, Valid
[jessie3] Task 2 (WP_parameter h): Valid, Valid, Valid, Valid, Valid
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment