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

Update proof for rmat_of_quat

parent 62a54a66
......@@ -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.8 } ],
"verdict": "valid", "time": 2.16 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.02 } ],
"verdict": "valid", "time": 4.28 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.69 } ],
"verdict": "valid", "time": 4.3 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -31,5 +31,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.06,
"time": 0.03,
"steps": 149234 } ] } } ] } } ] } } ] } } ]
......@@ -63,5 +63,5 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 9.1006,
"time": 8.0048,
"steps": 144 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -33,5 +33,5 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.997,
"time": 2.9,
"steps": 28 } ] } } ] } } ] } } ] } } ]
......@@ -31,7 +31,7 @@
{ "Unfold 'EqS12_RealVect3_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.0181,
"time": 0.0038,
"steps": 8 },
{ "header": "Split",
"tactic": "Wp.split",
......
......@@ -63,5 +63,5 @@
{ "Unfold 'EqS13_RealRMat_s'":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.03,
"time": 0.02,
"steps": 51791 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -193,5 +193,5 @@
{ "Unfold 'L_add_RealVect3'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.1478,
"time": 2.9623,
"steps": 142 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
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