Commit a5cb0535 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Adding is_finite preconditions and new postconditions

parent eb497c00
......@@ -578,7 +578,7 @@ Axiom S15_RealQuatVect_s_WhyType : WhyType S15_RealQuatVect_s.
Existing Instance S15_RealQuatVect_s_WhyType.
(* Why3 assumption *)
Definition F15_RealQuatVect_s_v (v:S15_RealQuatVect_s) : S12_RealVect3_s :=
Definition F15_RealQuatVect_s_vect (v:S15_RealQuatVect_s) : S12_RealVect3_s :=
match v with
| S15_RealQuatVect_s1 x x1 => x1
end.
......@@ -594,7 +594,7 @@ Definition F15_RealQuatVect_s_scalar (v:S15_RealQuatVect_s) :
Definition EqS15_RealQuatVect_s (S:S15_RealQuatVect_s)
(S1:S15_RealQuatVect_s) : Prop :=
((F15_RealQuatVect_s_scalar S1) = (F15_RealQuatVect_s_scalar S)) /\
EqS12_RealVect3_s (F15_RealQuatVect_s_v S) (F15_RealQuatVect_s_v S1).
EqS12_RealVect3_s (F15_RealQuatVect_s_vect S) (F15_RealQuatVect_s_vect S1).
(* Why3 assumption *)
Definition L_cross_product (v1:S12_RealVect3_s) (v2:S12_RealVect3_s) :
......@@ -668,8 +668,8 @@ Axiom Q_trans_add_RealVect3 :
(* Why3 assumption *)
Definition L_mult_RealQuatVect (q1:S15_RealQuatVect_s)
(q2:S15_RealQuatVect_s) : S15_RealQuatVect_s :=
let a := F15_RealQuatVect_s_v q1 in
let a1 := F15_RealQuatVect_s_v q2 in
let a := F15_RealQuatVect_s_vect q1 in
let a1 := F15_RealQuatVect_s_vect q2 in
let r := F15_RealQuatVect_s_scalar q1 in
let r1 := F15_RealQuatVect_s_scalar q2 in
S15_RealQuatVect_s1 (((-1%R)%R * (L_scalar_product a a1))%R + (r * r1)%R)%R
......@@ -677,6 +677,21 @@ Definition L_mult_RealQuatVect (q1:S15_RealQuatVect_s)
(L_add_RealVect3 (L_mult_scalar_1_ r a1) (L_mult_scalar_1_ r1 a))
(L_cross_product a a1)).
(* Why3 assumption *)
Definition L_conj_v_2_ (q:S15_RealQuatVect_s) : S15_RealQuatVect_s :=
S15_RealQuatVect_s1 (F15_RealQuatVect_s_scalar q)
(L_neg_vect (F15_RealQuatVect_s_vect q)).
(* Why3 assumption *)
Definition L_rotation_with_quat_1_ (q:S15_RealQuatVect_s)
(v:S15_RealQuatVect_s) : S15_RealQuatVect_s :=
L_mult_RealQuatVect (L_mult_RealQuatVect q v) (L_conj_v_2_ q).
(* Why3 assumption *)
Definition L_rotation_with_quat_2_ (q:S15_RealQuatVect_s)
(v:S12_RealVect3_s) : S15_RealQuatVect_s :=
L_rotation_with_quat_1_ q (S15_RealQuatVect_s1 0%R v).
(* Why3 assumption *)
Definition L_l_QuatVect_of_FloatQuat (Mf32:addr -> Reals.Rdefinitions.R)
(q:addr) : S15_RealQuatVect_s :=
......@@ -685,11 +700,9 @@ Definition L_l_QuatVect_of_FloatQuat (Mf32:addr -> Reals.Rdefinitions.R)
(Mf32 (shift q 3%Z))).
(* Why3 assumption *)
Definition L_conj_v_1_ (Mf32:addr -> Reals.Rdefinitions.R) (q:addr) :
S15_RealQuatVect_s :=
S15_RealQuatVect_s1 (Mf32 (shift q 0%Z))
(S12_RealVect3_s1 ((-1%R)%R * (Mf32 (shift q 1%Z)))%R
((-1%R)%R * (Mf32 (shift q 2%Z)))%R ((-1%R)%R * (Mf32 (shift q 3%Z)))%R).
Definition L_rotation_with_quat_3_ (Mf32:addr -> Reals.Rdefinitions.R)
(q:addr) (v:S12_RealVect3_s) : S15_RealQuatVect_s :=
L_rotation_with_quat_2_ (L_l_QuatVect_of_FloatQuat Mf32 q) v.
(* Why3 assumption *)
Definition L_mult_RealRMat (rmat1:S13_RealRMat_s) (rmat2:S13_RealRMat_s) :
......@@ -788,6 +801,11 @@ Axiom Q_mult_id_rmat_neutral :
(S13_RealRMat_s1 1%R 0%R 0%R 0%R 1%R 0%R 0%R 0%R 1%R))
rmat.
Axiom Q_mult_rmat_comm :
forall (rmat1:S13_RealRMat_s) (rmat2:S13_RealRMat_s),
EqS13_RealRMat_s (L_mult_RealRMat rmat1 rmat2)
(L_mult_RealRMat rmat2 rmat1).
Axiom Q_mult_rmat_id_neutral :
forall (rmat:S13_RealRMat_s),
EqS13_RealRMat_s
......@@ -842,11 +860,7 @@ Definition L_l_RMat_of_FloatQuat_1_ (Mf32:addr -> Reals.Rdefinitions.R)
Axiom Q_verify_rmat_of_quat_formula :
forall (Mf32:addr -> Reals.Rdefinitions.R) (q:addr) (v:addr),
let a := L_l_Vect_of_FloatVect3 Mf32 v in
EqS15_RealQuatVect_s
(L_mult_RealQuatVect
(L_mult_RealQuatVect (L_l_QuatVect_of_FloatQuat Mf32 q)
(S15_RealQuatVect_s1 0%R a))
(L_conj_v_1_ Mf32 q))
EqS15_RealQuatVect_s (L_rotation_with_quat_3_ Mf32 q a)
(S15_RealQuatVect_s1 0%R
(L_mult_RealRMat_RealVect3 (L_l_RMat_of_FloatQuat_1_ Mf32 q) a)).
......@@ -955,6 +969,13 @@ Axiom Q_equivalence_unary_pred :
P_unary_quaternion_2_ (L_l_Quat_of_FloatQuat Mf32 q) <->
P_unary_quaternion_1_ Mf32 q.
(* Why3 assumption *)
Definition L_conj_v_1_ (Mf32:addr -> Reals.Rdefinitions.R) (q:addr) :
S15_RealQuatVect_s :=
S15_RealQuatVect_s1 (Mf32 (shift q 0%Z))
(S12_RealVect3_s1 ((-1%R)%R * (Mf32 (shift q 1%Z)))%R
((-1%R)%R * (Mf32 (shift q 2%Z)))%R ((-1%R)%R * (Mf32 (shift q 3%Z)))%R).
(* Why3 assumption *)
Definition L_l_QuatVect_of_RealQuat (q:S14_RealQuat_s) : S15_RealQuatVect_s :=
S15_RealQuatVect_s1 (F14_RealQuat_s_qi q)
......
This diff is collapsed.
......@@ -18,7 +18,7 @@
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F13_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(L_transpose\n {\n F13_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]\n })",
"pattern": "L_transpose{RealRMat_s}[][][][][]" },
"children":
{ "Unfold 'L_transpose'":
......@@ -28,7 +28,7 @@
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_l_FloatQuat_of_RMat_0_max_1_\n {\n F13_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(L_l_FloatQuat_of_RMat_0_max_1_\n {\n F13_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]\n })",
"pattern": "L_l_FloatQuat_of_RMat_0_max_1_{RealRMat_s}" },
"children":
{ "Unfold 'L_l_FloatQuat_of_RMat_0_max_1_'":
......@@ -47,7 +47,7 @@
"params": {},
"select":
{ "select": "clause-goal",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 =\n (\\sqrt\n (1+Mf32_0[(shift_float32 a_0 0)]-Mf32_0[(shift_float32 a_0 4)]-\n Mf32_0[(shift_float32 a_0 8)])) in\nlet r_1 = (2*r_0) in\n(EqS14_RealQuat_s\n {\n F14_RealQuat_s_qi =\n (Mf32_0[(shift_float32 a_0 5)]-Mf32_0[(shift_float32 a_0 7)]) div r_1 ;\n F14_RealQuat_s_qx = 1/2*r_0 ;\n F14_RealQuat_s_qy =\n (Mf32_0[(shift_float32 a_0 1)]+Mf32_0[(shift_float32 a_0 3)]) div r_1 ;\n F14_RealQuat_s_qz =\n (Mf32_0[(shift_float32 a_0 2)]+Mf32_0[(shift_float32 a_0 6)]) div r_1\n }\n {\n F14_RealQuat_s_qi = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] ;\n F14_RealQuat_s_qx = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] ;\n F14_RealQuat_s_qy = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] ;\n F14_RealQuat_s_qz = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)]\n })",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 =\n (\\sqrt\n (1+Mf32_0[(shift_float32 a_0 0)]-Mf32_0[(shift_float32 a_0 4)]-\n Mf32_0[(shift_float32 a_0 8)])) in\nlet r_1 = (2*r_0) in\n(EqS14_RealQuat_s\n {\n F14_RealQuat_s_qi =\n (Mf32_0[(shift_float32 a_0 5)]-Mf32_0[(shift_float32 a_0 7)]) div r_1 ;\n F14_RealQuat_s_qx = 1/2*r_0 ;\n F14_RealQuat_s_qy =\n (Mf32_0[(shift_float32 a_0 1)]+Mf32_0[(shift_float32 a_0 3)]) div r_1 ;\n F14_RealQuat_s_qz =\n (Mf32_0[(shift_float32 a_0 2)]+Mf32_0[(shift_float32 a_0 6)]) div r_1\n }\n {\n F14_RealQuat_s_qi = Mf32_0[(shiftfield_F4_FloatQuat_qi q_0)] ;\n F14_RealQuat_s_qx = Mf32_0[(shiftfield_F4_FloatQuat_qx q_0)] ;\n F14_RealQuat_s_qy = Mf32_0[(shiftfield_F4_FloatQuat_qy q_0)] ;\n F14_RealQuat_s_qz = Mf32_0[(shiftfield_F4_FloatQuat_qz q_0)]\n })",
"pattern": "EqS14_RealQuat_s{RealQuat_s}{RealQuat_s}" },
"children":
{ "Unfold 'EqS14_RealQuat_s'":
......@@ -58,18 +58,16 @@
{ "select": "clause-step",
"at": 9,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 13.0899,
"steps": 762 } ],
"time": 8.5531,
"steps": 758 } ],
"Else":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.3846,
"steps": 988 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.9398,
"steps": 982 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.5036,
"steps": 1254 } ] } } ] } } ] } } ] } } ]
"time": 4.2827,
"steps": 1246 } ] } } ] } } ] } } ] } } ]
......@@ -58,8 +58,8 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.6657,
"steps": 1013 },
"time": 2.7437,
"steps": 999 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
[ { "prover": "script", "verdict": "valid", "time": 3.0907, "steps": 1331 },
{ "header": "Split", "tactic": "Wp.split", "params": {},
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 8, "kind": "branch",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children": { "Then": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 0.8195, "steps": 721 } ],
"time": 1.728, "steps": 717 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 3.0907, "steps": 1331 } ] } } ]
"time": 5.6067, "steps": 1323 } ] } } ]
......@@ -3,5 +3,5 @@
"target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
"children": { "Filter": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 5.9597,
"steps": 1628 } ] } } ]
"verdict": "valid", "time": 7.5488,
"steps": 1615 } ] } } ]
......@@ -70,8 +70,8 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.6229,
"steps": 809 },
"time": 4.0889,
"steps": 805 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
This diff is collapsed.
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m m_b2a_0) in\nlet a_1 = (shiftfield_F6_FloatRMat_m m_a2b_0) in\nlet m_0 = Mf32_9[(shift_float32 a_0 0)->Mf32_9[(shift_float32 a_1 0)]] in\nlet m_1 = m_0[(shift_float32 a_0 1)->m_0[(shift_float32 a_1 3)]] in\nlet m_2 = m_1[(shift_float32 a_0 2)->m_1[(shift_float32 a_1 6)]] in\nlet m_3 = m_2[(shift_float32 a_0 3)->m_2[(shift_float32 a_1 1)]] in\nlet m_4 = m_3[(shift_float32 a_0 4)->m_3[(shift_float32 a_1 4)]] in\nlet m_5 = m_4[(shift_float32 a_0 5)->m_4[(shift_float32 a_1 7)]] in\nlet m_6 = m_5[(shift_float32 a_0 6)->m_5[(shift_float32 a_1 2)]] in\nlet m_7 = m_6[(shift_float32 a_0 7)->m_6[(shift_float32 a_1 5)]] in\n(L_transpose\n (L_l_RMat_of_FloatRMat\n m_7[(shift_float32 a_0 8)->m_7[(shift_float32 a_1 8)]] m_a2b_0))",
"pattern": "L_transposeL_l_RMat_of_FloatRMat" },
"children": { "Unfold 'L_transpose'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m m_b2a_0) in\nlet a_1 = (shiftfield_F6_FloatRMat_m m_a2b_0) in\nlet m_0 = Mf32_9[(shift_float32 a_0 0)->Mf32_9[(shift_float32 a_1 0)]] in\nlet m_1 = m_0[(shift_float32 a_0 1)->m_0[(shift_float32 a_1 3)]] in\nlet m_2 = m_1[(shift_float32 a_0 2)->m_1[(shift_float32 a_1 6)]] in\nlet m_3 = m_2[(shift_float32 a_0 3)->m_2[(shift_float32 a_1 1)]] in\nlet m_4 = m_3[(shift_float32 a_0 4)->m_3[(shift_float32 a_1 4)]] in\nlet m_5 = m_4[(shift_float32 a_0 5)->m_4[(shift_float32 a_1 7)]] in\nlet m_6 = m_5[(shift_float32 a_0 6)->m_5[(shift_float32 a_1 2)]] in\nlet m_7 = m_6[(shift_float32 a_0 7)->m_6[(shift_float32 a_1 5)]] in\n(L_l_RMat_of_FloatRMat m_7[(shift_float32 a_0 8)->m_7[(shift_float32 a_1 8)]]\n m_b2a_0)",
"pattern": "L_l_RMat_of_FloatRMat[=]$m_b2a[=]" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "clause-goal",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m m_b2a_0) in\nlet a_1 = (shiftfield_F6_FloatRMat_m m_a2b_0) in\nlet r_0 = Mf32_9[(shift_float32 a_1 0)] in\nlet m_0 = Mf32_9[(shift_float32 a_0 0)->r_0] in\nlet r_1 = m_0[(shift_float32 a_1 3)] in\nlet m_1 = m_0[(shift_float32 a_0 1)->r_1] in\nlet r_2 = m_1[(shift_float32 a_1 6)] in\nlet m_2 = m_1[(shift_float32 a_0 2)->r_2] in\nlet r_3 = m_2[(shift_float32 a_1 1)] in\nlet m_3 = m_2[(shift_float32 a_0 3)->r_3] in\nlet r_4 = m_3[(shift_float32 a_1 4)] in\nlet m_4 = m_3[(shift_float32 a_0 4)->r_4] in\nlet r_5 = m_4[(shift_float32 a_1 7)] in\nlet m_5 = m_4[(shift_float32 a_0 5)->r_5] in\nlet r_6 = m_5[(shift_float32 a_1 2)] in\nlet m_6 = m_5[(shift_float32 a_0 6)->r_6] in\nlet r_7 = m_6[(shift_float32 a_1 5)] in\nlet m_7 = m_6[(shift_float32 a_0 7)->r_7] in\nlet r_8 = m_7[(shift_float32 a_1 8)] in\nlet a_2 = (L_l_RMat_of_FloatRMat m_7[(shift_float32 a_0 8)->r_8] m_a2b_0) in\n(EqS13_RealRMat_s\n {\n a_2 with\n F13_RealRMat_s_a01 = a_2.F13_RealRMat_s_a10 ;\n F13_RealRMat_s_a02 = a_2.F13_RealRMat_s_a20 ;\n F13_RealRMat_s_a10 = a_2.F13_RealRMat_s_a01 ;\n F13_RealRMat_s_a12 = a_2.F13_RealRMat_s_a21 ;\n F13_RealRMat_s_a20 = a_2.F13_RealRMat_s_a02 ;\n F13_RealRMat_s_a21 = a_2.F13_RealRMat_s_a12\n }\n {\n F13_RealRMat_s_a00 = r_0 ;\n F13_RealRMat_s_a01 = r_1 ;\n F13_RealRMat_s_a02 = r_2 ;\n F13_RealRMat_s_a10 = r_3 ;\n F13_RealRMat_s_a11 = r_4 ;\n F13_RealRMat_s_a12 = r_5 ;\n F13_RealRMat_s_a20 = r_6 ;\n F13_RealRMat_s_a21 = r_7 ;\n F13_RealRMat_s_a22 = r_8\n })",
"pattern": "EqS13_RealRMat_s{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'EqS13_RealRMat_s'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m m_b2a_0) in\nlet a_1 = (shiftfield_F6_FloatRMat_m m_a2b_0) in\nlet m_0 = Mf32_9[(shift_float32 a_0 0)->Mf32_9[(shift_float32 a_1 0)]] in\nlet m_1 = m_0[(shift_float32 a_0 1)->m_0[(shift_float32 a_1 3)]] in\nlet m_2 = m_1[(shift_float32 a_0 2)->m_1[(shift_float32 a_1 6)]] in\nlet m_3 = m_2[(shift_float32 a_0 3)->m_2[(shift_float32 a_1 1)]] in\nlet m_4 = m_3[(shift_float32 a_0 4)->m_3[(shift_float32 a_1 4)]] in\nlet m_5 = m_4[(shift_float32 a_0 5)->m_4[(shift_float32 a_1 7)]] in\nlet m_6 = m_5[(shift_float32 a_0 6)->m_5[(shift_float32 a_1 2)]] in\nlet m_7 = m_6[(shift_float32 a_0 7)->m_6[(shift_float32 a_1 5)]] in\n(L_l_RMat_of_FloatRMat m_7[(shift_float32 a_0 8)->m_7[(shift_float32 a_1 8)]]\n m_a2b_0)",
"pattern": "L_l_RMat_of_FloatRMat[=]$m_a2b[=]" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 10.519,
"steps": 11772 } ] } } ] } } ] } } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in\nlet r_1 = (\\sin r_0) in\nlet r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in\nlet r_3 = (\\sin r_2) in\nlet r_4 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in\nlet r_5 = (\\sin r_4) in\nlet r_6 = (\\cos r_2) in\nlet r_7 = (\\cos r_4) in\nlet r_8 = (\\cos r_0) in\n(L_l_RMat_of_FloatRMat\n Mf32_9[(shift_float32 a_0 0)->(r_6*r_7)-(r_1*r_3*r_5)]\n [(shift_float32 a_0 1)->(r_3*r_7)+(r_1*r_5*r_6)][(shift_float32 a_0 2)\n ->-1*r_5*r_8][(shift_float32 a_0 3)->-1*r_3*r_8][(shift_float32 a_0 4)\n ->r_8*r_6][(shift_float32 a_0 5)->r_1][(shift_float32 a_0 6)\n ->(r_5*r_6)+(r_1*r_3*r_7)][(shift_float32 a_0 7)\n ->(r_3*r_5)-(r_1*r_6*r_7)][(shift_float32 a_0 8)->r_8*r_7] rm_0)",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_9[(shiftfield_F7_FloatEulers_phi e_1)] in\nlet r_1 = (\\sin r_0) in\nlet r_2 = Mf32_9[(shiftfield_F7_FloatEulers_psi e_1)] in\nlet r_3 = (\\sin r_2) in\nlet r_4 = Mf32_9[(shiftfield_F7_FloatEulers_theta e_1)] in\nlet r_5 = (\\sin r_4) in\nlet r_6 = (\\cos r_2) in\nlet r_7 = (\\cos r_4) in\nlet r_8 = (\\cos r_0) in\n(L_l_RMat_of_FloatRMat\n Mf32_9[(shift_float32 a_0 0)->(r_6*r_7)-(r_1*r_3*r_5)]\n [(shift_float32 a_0 1)->(r_3*r_7)+(r_1*r_5*r_6)][(shift_float32 a_0 2)\n ->-1*r_5*r_8][(shift_float32 a_0 3)->-1*r_3*r_8][(shift_float32 a_0 4)\n ->r_8*r_6][(shift_float32 a_0 5)->r_1][(shift_float32 a_0 6)\n ->(r_5*r_6)+(r_1*r_3*r_7)][(shift_float32 a_0 7)\n ->(r_3*r_5)-(r_1*r_6*r_7)][(shift_float32 a_0 8)->r_8*r_7] rm_0)",
"pattern": "L_l_RMat_of_FloatRMat[=]$rm[=]shift_float32" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "clause-goal",
"target": "let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in\nlet r_1 = (\\sin r_0) in\nlet r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in\nlet r_3 = (\\sin r_2) in\nlet r_4 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in\nlet r_5 = (\\sin r_4) in\nlet r_6 = (\\cos r_2) in\nlet r_7 = (\\cos r_4) in\nlet r_8 = (\\cos r_0) in\n(P_special_orthogonal\n {\n F13_RealRMat_s_a00 = (r_6*r_7)-(r_1*r_3*r_5) ;\n F13_RealRMat_s_a01 = (r_3*r_7)+(r_1*r_5*r_6) ;\n F13_RealRMat_s_a02 = -1*r_5*r_8 ;\n F13_RealRMat_s_a10 = -1*r_3*r_8 ;\n F13_RealRMat_s_a11 = r_8*r_6 ;\n F13_RealRMat_s_a12 = r_1 ;\n F13_RealRMat_s_a20 = (r_5*r_6)+(r_1*r_3*r_7) ;\n F13_RealRMat_s_a21 = (r_3*r_5)-(r_1*r_6*r_7) ;\n F13_RealRMat_s_a22 = r_8*r_7\n })",
"target": "let r_0 = Mf32_9[(shiftfield_F7_FloatEulers_phi e_1)] in\nlet r_1 = (\\sin r_0) in\nlet r_2 = Mf32_9[(shiftfield_F7_FloatEulers_psi e_1)] in\nlet r_3 = (\\sin r_2) in\nlet r_4 = Mf32_9[(shiftfield_F7_FloatEulers_theta e_1)] in\nlet r_5 = (\\sin r_4) in\nlet r_6 = (\\cos r_2) in\nlet r_7 = (\\cos r_4) in\nlet r_8 = (\\cos r_0) in\n(P_special_orthogonal\n {\n F13_RealRMat_s_a00 = (r_6*r_7)-(r_1*r_3*r_5) ;\n F13_RealRMat_s_a01 = (r_3*r_7)+(r_1*r_5*r_6) ;\n F13_RealRMat_s_a02 = -1*r_5*r_8 ;\n F13_RealRMat_s_a10 = -1*r_3*r_8 ;\n F13_RealRMat_s_a11 = r_8*r_6 ;\n F13_RealRMat_s_a12 = r_1 ;\n F13_RealRMat_s_a20 = (r_5*r_6)+(r_1*r_3*r_7) ;\n F13_RealRMat_s_a21 = (r_3*r_5)-(r_1*r_6*r_7) ;\n F13_RealRMat_s_a22 = r_8*r_7\n })",
"pattern": "P_special_orthogonal{RealRMat_s}" },
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.3514,
"time": 2.9475,
"steps": 102 } ] } } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in\nlet r_1 = (\\cos r_0) in\nlet r_2 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in\nlet r_3 = (\\cos r_2) in\nlet r_4 = (\\sin r_0) in\nlet r_5 = (\\sin r_2) in\nlet r_6 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in\nlet r_7 = (\\cos r_6) in\nlet r_8 = (\\sin r_6) in\n(L_l_RMat_of_FloatRMat\n Mf32_9[(shift_float32 a_0 0)->r_1*r_3][(shift_float32 a_0 1)->r_4*r_3]\n [(shift_float32 a_0 2)->-r_5][(shift_float32 a_0 3)\n ->(r_8*r_5*r_1)-(r_4*r_7)][(shift_float32 a_0 4)\n ->(r_7*r_1)+(r_8*r_4*r_5)][(shift_float32 a_0 5)->r_8*r_3]\n [(shift_float32 a_0 6)->(r_8*r_4)+(r_5*r_7*r_1)][(shift_float32 a_0 7)\n ->(r_4*r_5*r_7)-(r_8*r_1)][(shift_float32 a_0 8)->r_7*r_3] rm_0)",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_9[(shiftfield_F7_FloatEulers_psi e_1)] in\nlet r_1 = (\\cos r_0) in\nlet r_2 = Mf32_9[(shiftfield_F7_FloatEulers_theta e_1)] in\nlet r_3 = (\\cos r_2) in\nlet r_4 = (\\sin r_0) in\nlet r_5 = (\\sin r_2) in\nlet r_6 = Mf32_9[(shiftfield_F7_FloatEulers_phi e_1)] in\nlet r_7 = (\\cos r_6) in\nlet r_8 = (\\sin r_6) in\n(L_l_RMat_of_FloatRMat\n Mf32_9[(shift_float32 a_0 0)->r_1*r_3][(shift_float32 a_0 1)->r_4*r_3]\n [(shift_float32 a_0 2)->-r_5][(shift_float32 a_0 3)\n ->(r_8*r_5*r_1)-(r_4*r_7)][(shift_float32 a_0 4)\n ->(r_7*r_1)+(r_8*r_4*r_5)][(shift_float32 a_0 5)->r_8*r_3]\n [(shift_float32 a_0 6)->(r_8*r_4)+(r_5*r_7*r_1)][(shift_float32 a_0 7)\n ->(r_4*r_5*r_7)-(r_8*r_1)][(shift_float32 a_0 8)->r_7*r_3] rm_0)",
"pattern": "L_l_RMat_of_FloatRMat[=]$rm[=]shift_float32" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "clause-goal",
"target": "let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in\nlet r_1 = (\\cos r_0) in\nlet r_2 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in\nlet r_3 = (\\cos r_2) in\nlet r_4 = (\\sin r_0) in\nlet r_5 = (\\sin r_2) in\nlet r_6 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in\nlet r_7 = (\\cos r_6) in\nlet r_8 = (\\sin r_6) in\n(P_special_orthogonal\n {\n F13_RealRMat_s_a00 = r_1*r_3 ;\n F13_RealRMat_s_a01 = r_4*r_3 ;\n F13_RealRMat_s_a02 = -r_5 ;\n F13_RealRMat_s_a10 = (r_8*r_5*r_1)-(r_4*r_7) ;\n F13_RealRMat_s_a11 = (r_7*r_1)+(r_8*r_4*r_5) ;\n F13_RealRMat_s_a12 = r_8*r_3 ;\n F13_RealRMat_s_a20 = (r_8*r_4)+(r_5*r_7*r_1) ;\n F13_RealRMat_s_a21 = (r_4*r_5*r_7)-(r_8*r_1) ;\n F13_RealRMat_s_a22 = r_7*r_3\n })",
"target": "let r_0 = Mf32_9[(shiftfield_F7_FloatEulers_psi e_1)] in\nlet r_1 = (\\cos r_0) in\nlet r_2 = Mf32_9[(shiftfield_F7_FloatEulers_theta e_1)] in\nlet r_3 = (\\cos r_2) in\nlet r_4 = (\\sin r_0) in\nlet r_5 = (\\sin r_2) in\nlet r_6 = Mf32_9[(shiftfield_F7_FloatEulers_phi e_1)] in\nlet r_7 = (\\cos r_6) in\nlet r_8 = (\\sin r_6) in\n(P_special_orthogonal\n {\n F13_RealRMat_s_a00 = r_1*r_3 ;\n F13_RealRMat_s_a01 = r_4*r_3 ;\n F13_RealRMat_s_a02 = -r_5 ;\n F13_RealRMat_s_a10 = (r_8*r_5*r_1)-(r_4*r_7) ;\n F13_RealRMat_s_a11 = (r_7*r_1)+(r_8*r_4*r_5) ;\n F13_RealRMat_s_a12 = r_8*r_3 ;\n F13_RealRMat_s_a20 = (r_8*r_4)+(r_5*r_7*r_1) ;\n F13_RealRMat_s_a21 = (r_4*r_5*r_7)-(r_8*r_1) ;\n F13_RealRMat_s_a22 = r_7*r_3\n })",
"pattern": "P_special_orthogonal{RealRMat_s}" },
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.34,
"time": 3.1177,
"steps": 102 } ] } } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 20. },
{ "prover": "script", "verdict": "valid" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "True": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout", "time": 20. },
{ "header": "Separated",
"children": { "True": [ { "header": "Separated",
"tactic": "Wp.separated", "params": {},
"select": { "select": "clause-step", "at": 2,
"kind": "have",
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 8.49 } ],
"OnLeft": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"time": 7.76 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 13.72 } ],
"OnRight": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"time": 12.1 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 15.68 } ],
"time": 11.83 } ],
"OverLap": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"False": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 20. },
{ "prover": "script", "verdict": "valid" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "True": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout", "time": 20. },
{ "header": "Separated",
"children": { "True": [ { "header": "Separated",
"tactic": "Wp.separated", "params": {},
"select": { "select": "clause-step", "at": 2,
"kind": "have",
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 3.82 } ],
"OnLeft": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"time": 4.25 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.37 } ],
"OnRight": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"time": 6.4 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.47 } ],
"time": 5.93 } ],
"OverLap": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"False": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 2.41 } ],
"verdict": "valid", "time": 2.36 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5. } ],
"verdict": "valid", "time": 4.7 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.84 } ],
"verdict": "valid", "time": 4.6 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 20. },
{ "prover": "script", "verdict": "valid" },
{ "header": "Split", "tactic": "Wp.split", "params": {},
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "True": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout", "time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 20. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout", "time": 20. },
{ "header": "Separated",
"children": { "True": [ { "header": "Separated",
"tactic": "Wp.separated", "params": {},
"select": { "select": "clause-step", "at": 2,
"kind": "have",
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "Alt-Ergo:2.3.3",
"children": { "WrongBase": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 14.1908,
"time": 13.8324,
"steps": 136 } ],
"OnLeft": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 20.95 },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 20. } ],
"OnRight": [ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 20. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "failed" },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 20. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 20. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 20. },
{ "header": "Range",
"time": 16.72 } ],
"OnRight": [ { "header": "Range",
"tactic": "Wp.range",