From faa719b37a2a8c16d30bed6cf73180b97b965125 Mon Sep 17 00:00:00 2001 From: lukstafi Date: Tue, 3 Mar 2015 17:26:17 +0100 Subject: [PATCH] Fix to the verification optimization: only check conclusion variables. --- src/Abduction.ml | 5 +- src/NumS.ml | 6 +- test.log | 709 ++++++++++++++++++++++++----------------------- 3 files changed, 371 insertions(+), 349 deletions(-) diff --git a/src/Abduction.ml b/src/Abduction.ml index b256522..40631b1 100644 --- a/src/Abduction.ml +++ b/src/Abduction.ml @@ -892,10 +892,7 @@ let abd q ~bvs ~xbvs ?orig_ren ?b_of_v ~upward_of ~nonparam_vars neg_brs in let verif_brs = List.map2 (fun (prem, concl_ty) (_, _, _, concl_num) -> - VarSet.union (fvs_sb prem.cnj_typ) - (VarSet.union (NumDefs.fvs_formula prem.cnj_num) - (VarSet.union (fvs_sb concl_ty) - (NumDefs.fvs_formula concl_num))), + VarSet.union (fvs_sb concl_ty) (NumDefs.fvs_formula concl_num), prem, concl_ty, concl_num) brs_typ brs_num in let validate added_vs (vs, ans) = diff --git a/src/NumS.ml b/src/NumS.ml index 0d3142b..31979a6 100644 --- a/src/NumS.ml +++ b/src/NumS.ml @@ -2374,10 +2374,10 @@ let subst_chi chi_sb pos_chi = let empty_renaming = Hashtbl.create 0 let empty_b_of_v v = v -let fvs_br (_, _, _, (d_eqn, d_ineqn), +let fvs_br_concl (_, _, _, _, (c_eqn, c_ineqn, c_optis, c_suboptis)) = VarSet.union - (vars_of_map (vars_of_map fvs_w) [d_eqn; d_ineqn; c_eqn; c_ineqn]) + (vars_of_map (vars_of_map fvs_w) [c_eqn; c_ineqn]) (vars_of_map (vars_of_map fvs_2w) [c_optis; c_suboptis]) let fvs_sep_w_formula (c_eqn, c_ineqn, c_optis, c_suboptis) = @@ -2526,7 +2526,7 @@ let abd q ~bvs ~xbvs ?(orig_ren=empty_renaming) ?(b_of_v=empty_b_of_v) else let brs_n = List.length res in let brs_r = ref brs_n in - List.map (fun br -> br, (fvs_br br, brs_r, brs_n, br)) res) + List.map (fun br -> br, (fvs_br_concl br, brs_r, brs_n, br)) res) brs in let brs, validate_brs = List.split brs in (*[* Format.printf "NumS.abd: brs processing past merging@\n%!"; *]*) diff --git a/test.log b/test.log index 9276198..d87f9b2 100644 --- a/test.log +++ b/test.log @@ -1,14 +1,34 @@ -Compilation started at Fri Feb 27 04:45:47 +Compilation started at Tue Mar 3 16:57:04 make testnative ocamlbuild src/Tests.native -lib nums -pkg oUnit -- Warning: tag "package" does not expect a parameter, but is used with parameter "oUnit" /home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/AbductionTest.ml > src/AbductionTest.ml.depends +/home/lukstafi/.opam/4.01.0/bin/ocamlc.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Defs.cmi src/Defs.mli +/home/lukstafi/.opam/4.01.0/bin/ocamlc.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Aux.cmo src/Aux.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlc.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/NumDefs.cmi src/NumDefs.mli +/home/lukstafi/.opam/4.01.0/bin/ocamlc.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/OrderDefs.cmo src/OrderDefs.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlc.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Terms.cmi src/Terms.mli /home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/DisjElimTest.ml > src/DisjElimTest.ml.depends +/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/NumSTest.ml > src/NumSTest.ml.depends /home/lukstafi/.opam/4.01.0/bin/ocamlc.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/AbductionTest.cmo src/AbductionTest.ml /home/lukstafi/.opam/4.01.0/bin/ocamlc.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/DisjElimTest.cmo src/DisjElimTest.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlc.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/NumSTest.cmo src/NumSTest.ml +/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/Abduction.ml > src/Abduction.ml.depends +/home/lukstafi/.opam/4.01.0/bin/ocamldep.opt -modules src/NumS.ml > src/NumS.ml.depends +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/NumS.cmx src/NumS.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Infer.cmx src/Infer.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Abduction.cmx src/Abduction.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/DisjElim.cmx src/DisjElim.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Invariants.cmx src/Invariants.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/InvarGenT.cmx src/InvarGenT.ml /home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/AbductionTest.cmx src/AbductionTest.ml /home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/DisjElimTest.cmx src/DisjElimTest.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/InferTest.cmx src/InferTest.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/InvarGenTTest.cmx src/InvarGenTTest.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/InvariantsTest.cmx src/InvariantsTest.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/NumSTest.cmx src/NumSTest.ml +/home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt -c -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml -I src -o src/Tests.cmx src/Tests.ml /home/lukstafi/.opam/4.01.0/bin/ocamlopt.opt nums.cmxa -I /home/lukstafi/.opam/4.01.0/lib/oUnit -I /home/lukstafi/.opam/4.01.0/lib/ocaml unix.cmxa oUnit.cmxa src/Aux.cmx src/Defs.cmx src/NumDefs.cmx src/OrderDefs.cmx src/Terms.cmx src/Joint.cmx src/NumS.cmx src/OrderS.cmx src/Infer.cmx src/Abduction.cmx src/Parser.cmx src/Lexer.cmx src/AbductionTest.cmx src/DisjElim.cmx src/DisjElimTest.cmx src/InferTest.cmx src/Invariants.cmx src/OCaml.cmx src/InvarGenT.cmx src/InvarGenTTest.cmx src/InvariantsTest.cmx src/NumSTest.cmx src/OrderSTest.cmx src/TermsTest.cmx src/Tests.cmx -o src/Tests.native InvarGenT:0:Terms:0:parsing and printing ... ok @@ -37,145 +57,145 @@ ok InvarGenT:5:DisjElim:1:simplified eval ... ok InvarGenT:6:Invariants:0:simple eval ... - t=0.013s ok + t=0.017s ok InvarGenT:6:Invariants:1:simple assert false ... t=0.003s ok InvarGenT:6:Invariants:2:foo without when 1 ... - t=0.001s ok + t=0.002s ok InvarGenT:6:Invariants:3:foo without when 2 ... t=0.003s ok InvarGenT:6:Invariants:4:foo with when 1 ... t=0.005s ok InvarGenT:6:Invariants:5:foo with when 2 ... - t=0.003s ok + t=0.002s ok InvarGenT:6:Invariants:6:deadcode foo ... t=0.003s ok InvarGenT:6:Invariants:7:deadcode foo fail ... ok InvarGenT:6:Invariants:8:abs ... - t=0.012s ok + t=0.011s ok InvarGenT:6:Invariants:9:abs2 ... t=0.012s ok InvarGenT:6:Invariants:10:eval ... - t=0.103s ok + t=0.115s ok InvarGenT:6:Invariants:11:eval hard ... - t=0.085s ok + t=0.086s ok InvarGenT:6:Invariants:12:equal1 wrong type ... - t=0.240s ok + t=0.229s ok InvarGenT:6:Invariants:13:equal with test ... - t=0.472s ok + t=0.413s ok InvarGenT:6:Invariants:14:equal with assert ... - t=1.813s ok + t=1.351s ok InvarGenT:6:Invariants:15:equal with assert and test ... - t=0.754s ok + t=0.651s ok InvarGenT:6:Invariants:16:SPJ non-principal 1 ... - t=0.002s ok -InvarGenT:6:Invariants:17:SPJ non-principal 2 ... t=0.003s ok +InvarGenT:6:Invariants:17:SPJ non-principal 2 ... + t=0.005s ok InvarGenT:6:Invariants:18:TS infinitely non-principal ... - t=0.002s ok + t=0.003s ok InvarGenT:6:Invariants:19:TS non-principal subexpr ... - t=0.004s ok + t=0.003s ok InvarGenT:6:Invariants:20:TS non-principal subexpr 2 ... ok InvarGenT:6:Invariants:21:simple existential ... - t=0.023s ok + t=0.022s ok InvarGenT:6:Invariants:22:simple universal ... - t=0.005s ok + t=0.007s ok InvarGenT:6:Invariants:23:simple existential 2 ... - t=0.042s ok + t=0.039s ok InvarGenT:6:Invariants:24:map mono ... - t=0.006s ok + t=0.005s ok InvarGenT:6:Invariants:25:append expanded ... t=0.023s ok InvarGenT:6:Invariants:26:append asserted ... - t=0.023s ok + t=0.024s ok InvarGenT:6:Invariants:27:interleave ... - t=0.019s ok + t=0.016s ok InvarGenT:6:Invariants:28:interleave 3 ... - t=0.175s ok + t=0.160s ok InvarGenT:6:Invariants:29:binary increment ... - t=0.009s ok + t=0.011s ok InvarGenT:6:Invariants:30:binary plus expanded ... - t=0.825s ok + t=0.760s ok InvarGenT:6:Invariants:31:binary plus asserted ... - t=0.931s ok + t=0.888s ok InvarGenT:6:Invariants:32:binary plus with test ... - t=0.933s ok + t=0.880s ok InvarGenT:6:Invariants:33:flatten_pairs ... - t=0.015s ok + t=0.019s ok InvarGenT:6:Invariants:34:escape castle ... - t=0.153s ok + t=0.130s ok InvarGenT:6:Invariants:35:easy nested universal ... - t=0.029s ok + t=0.028s ok InvarGenT:6:Invariants:36:equational nested universal ... - t=1.933s ok + t=1.602s ok InvarGenT:6:Invariants:37:double nested universal ... - t=0.053s ok + t=0.050s ok InvarGenT:6:Invariants:38:find castle ... t=0.022s ok InvarGenT:6:Invariants:39:find castle big ... - t=0.044s ok + t=0.041s ok InvarGenT:6:Invariants:40:search castle shortcut ... t=0.026s ok InvarGenT:6:Invariants:41:search castle distance ... t=0.044s ok InvarGenT:6:Invariants:42:search castle distance A/B ... - t=0.072s ok + t=0.061s ok InvarGenT:6:Invariants:43:castle not existential ... - t=0.012s ok + t=0.013s ok InvarGenT:6:Invariants:44:castle nested not existential ... t=0.021s ok InvarGenT:6:Invariants:45:castle nested existential factored ... - t=0.026s ok + t=0.024s ok InvarGenT:6:Invariants:46:castle nested existential ... - t=0.025s ok + t=0.026s ok InvarGenT:6:Invariants:47:existential by hand ... - t=0.020s ok + t=0.021s ok InvarGenT:6:Invariants:48:existential with param ... - t=0.085s ok + t=0.073s ok InvarGenT:6:Invariants:49:universal option ... - t=0.006s ok + t=0.008s ok InvarGenT:6:Invariants:50:existential option ... - t=0.024s ok + t=0.023s ok InvarGenT:6:Invariants:51:not existential option ... - t=0.042s ok + t=0.040s ok InvarGenT:6:Invariants:52:non-num map not existential poly ... t=0.036s ok InvarGenT:6:Invariants:53:non-num map not existential mono ... - t=0.015s ok + t=0.014s ok InvarGenT:6:Invariants:54:map not existential mono ... t=0.017s ok InvarGenT:6:Invariants:55:map not existential poly ... - t=0.062s ok + t=0.065s ok InvarGenT:6:Invariants:56:map not existential instance ... - t=0.032s ok + t=0.028s ok InvarGenT:6:Invariants:57:filter mono ... - t=0.135s ok + t=0.115s ok InvarGenT:6:Invariants:58:filter Bar ... - t=0.167s ok + t=0.140s ok InvarGenT:6:Invariants:59:filter poly ... - t=0.337s ok + t=0.295s ok InvarGenT:6:Invariants:60:poly filter map ... - t=0.476s ok + t=0.426s ok InvarGenT:6:Invariants:61:binary upper bound-wrong ... - t=1.680s ok + t=1.110s ok InvarGenT:6:Invariants:62:binary upper bound expanded ... - t=2.424s ok + t=1.590s ok InvarGenT:6:Invariants:63:nested recursion simple eval ... - t=0.013s ok + t=0.015s ok InvarGenT:6:Invariants:64:nested recursion eval ... - t=0.107s ok + t=0.103s ok InvarGenT:6:Invariants:65:mutual recursion simple calc ... - t=0.091s ok + t=0.082s ok InvarGenT:6:Invariants:66:mutual recursion medium calc ... - t=0.139s ok + t=0.135s ok InvarGenT:6:Invariants:67:mutual recursion calc ... - t=0.763s ok + t=0.634s ok InvarGenT:6:Invariants:68:local defs simple ... - t=0.005s ok + t=0.007s ok InvarGenT:6:Invariants:69:local recursion simple ... - t=0.016s ok + t=0.018s ok InvarGenT:6:Invariants:70:nonrec simple ... t=0.000s ok InvarGenT:6:Invariants:71:binomial heap--rank ... @@ -183,204 +203,209 @@ InvarGenT:6:Invariants:71:binomial heap--rank ... InvarGenT:6:Invariants:72:binomial heap--link ... t=0.024s ok InvarGenT:6:Invariants:73:unary minimum expanded ... - t=0.278s ok + t=0.236s ok InvarGenT:6:Invariants:74:unary minimum asserted 1 ... - t=0.342s ok + t=0.295s ok InvarGenT:6:Invariants:75:unary minimum asserted 2 ... - t=0.344s ok + t=0.294s ok InvarGenT:6:Invariants:76:unary minimum asserted 3 ... - t=0.514s ok + t=0.460s ok InvarGenT:6:Invariants:77:list zip prefix expanded ... - t=0.772s ok + t=0.678s ok InvarGenT:6:Invariants:78:unary maximum expanded ... - t=0.099s ok + t=0.083s ok InvarGenT:6:Invariants:79:list map2 with postfix expanded ... - t=0.255s ok + t=0.223s ok InvarGenT:6:Invariants:80:list filter-zip prefix ... - t=1.265s ok + t=1.120s ok InvarGenT:6:Invariants:81:list filter-map2 with postfix ... - t=1.206s ok + t=1.013s ok InvarGenT:6:Invariants:82:list filter-map2 with filter postfix mono ... - t=1.504s ok + t=1.223s ok InvarGenT:6:Invariants:83:non-num no postcond list filter-map2 with filter postfix ... - t=0.242s ok + t=0.245s ok InvarGenT:6:Invariants:84:non-num list filter-map2 with filter postfix ... - t=1.992s ok + t=1.672s ok InvarGenT:6:Invariants:85:list filter-map2 with filter postfix ... - t=8.042s ok + t=6.455s ok InvarGenT:6:Invariants:86:list map2 with filter postfix ... - t=6.229s ok + t=5.215s ok InvarGenT:6:Invariants:87:avl_tree--height ... - t=0.006s ok + t=0.008s ok InvarGenT:6:Invariants:88:avl_tree--create ... - t=0.122s ok + t=0.109s ok InvarGenT:6:Invariants:89:avl_tree--create2 ... - t=0.115s ok + t=0.113s ok InvarGenT:6:Invariants:90:avl_tree--singleton ... - t=0.004s ok + t=0.006s ok InvarGenT:6:Invariants:91:avl_tree--min_binding ... - t=0.035s ok + t=0.034s ok InvarGenT:6:Invariants:92:avl_tree--rotr-simple ... - t=4.017s ok + t=3.427s ok InvarGenT:6:Invariants:93:avl_tree--rotr-simple2 ... - t=2.131s ok + t=1.556s ok InvarGenT:6:Invariants:94:avl_tree--rotr-simple3 ... - t=2.333s ok + t=1.712s ok InvarGenT:6:Invariants:95:avl_tree--rotr ... - t=1.628s ok + t=1.194s ok InvarGenT:6:Invariants:96:avl_tree--rotl-simple ... - t=3.974s ok + t=3.308s ok InvarGenT:6:Invariants:97:avl_tree--rotl-simple2 ... - t=1.565s ok + t=1.159s ok InvarGenT:6:Invariants:98:avl_tree--rotl ... - t=1.642s ok + t=1.219s ok InvarGenT:6:Invariants:99:avl_tree--add-simple ... - t=0.832s ok + t=0.780s ok InvarGenT:6:Invariants:100:avl_tree--add-simple2 ... - t=0.846s ok + t=0.670s ok InvarGenT:6:Invariants:101:avl_tree--add ... - t=1.482s ok + t=1.149s ok InvarGenT:6:Invariants:102:avl_tree--add2 ... - t=1.461s ok + t=1.043s ok InvarGenT:6:Invariants:103:avl_tree--add-harder ... - t=1.216s ok + t=1.080s ok InvarGenT:6:Invariants:104:avl_tree--remove_min_binding-simple ... - t=1.003s ok + t=0.897s ok InvarGenT:6:Invariants:105:avl_tree--remove_min_binding ... - t=3.239s ok + t=2.469s ok InvarGenT:6:Invariants:106:avl_tree--remove_min_binding-harder ... - t=2.746s ok + t=2.301s ok InvarGenT:6:Invariants:107:avl_tree--merge-simple ... - t=1.207s ok + t=1.078s ok InvarGenT:6:Invariants:108:avl_tree--merge ... - t=2.478s ok + t=1.880s ok InvarGenT:6:Invariants:109:avl_tree--merge2 ... - t=1.989s ok + t=1.354s ok InvarGenT:6:Invariants:110:avl_tree--merge3 ... TODO InvarGenT:6:Invariants:111:avl_tree--merge4 ... - t=1.458s ok + t=1.079s ok InvarGenT:6:Invariants:112:avl_tree--remove-simple ... - t=0.652s ok + t=0.534s ok InvarGenT:6:Invariants:113:avl_tree--remove ... - t=0.975s ok + t=0.684s ok InvarGenT:6:Invariants:114:avl_tree--remove2 ... - t=0.983s ok + t=0.681s ok InvarGenT:6:Invariants:115:avl_tree--remove-harder ... - t=0.789s ok + t=0.600s ok InvarGenT:7:InvarGenT:0:simple eval ... InvarGenT: Generated file ./examples/simple_eval.gadti InvarGenT: Generated file ./examples/simple_eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/simple_eval.ml" exited with code 0 - t=0.015s ok + t=0.023s ok InvarGenT:7:InvarGenT:1:eval ... InvarGenT: Generated file ./examples/eval.gadti InvarGenT: Generated file ./examples/eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/eval.ml" exited with code 0 - t=0.101s ok + t=0.097s ok InvarGenT:7:InvarGenT:2:simple when ... InvarGenT: Generated file ./examples/simple_when.gadti InvarGenT: Generated file ./examples/simple_when.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/simple_when.ml" exited with code 0 - t=0.005s ok + t=0.006s ok InvarGenT:7:InvarGenT:3:equal1_wrong ... InvarGenT: Generated file ./examples/equal1_wrong.gadti InvarGenT: Generated file ./examples/equal1_wrong.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equal1_wrong.ml" exited with code 0 - t=0.238s ok + t=0.246s ok InvarGenT:7:InvarGenT:4:equal_test ... InvarGenT: Generated file ./examples/equal_test.gadti InvarGenT: Generated file ./examples/equal_test.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equal_test.ml" exited with code 0 - t=0.474s ok + t=0.421s ok InvarGenT:7:InvarGenT:5:equal_assert ... InvarGenT: Generated file ./examples/equal_assert.gadti InvarGenT: Generated file ./examples/equal_assert.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equal_assert.ml" exited with code 0 - t=1.798s ok + t=1.341s ok InvarGenT:7:InvarGenT:6:binary_plus ... InvarGenT: Generated file ./examples/binary_plus.gadti InvarGenT: Generated file ./examples/binary_plus.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/binary_plus.ml" exited with code 0 - t=0.828s ok + t=0.778s ok InvarGenT:7:InvarGenT:7:binary_plus-harder ... TODO InvarGenT:7:InvarGenT:8:flatten_pairs ... InvarGenT: Generated file ./examples/flatten_pairs.gadti InvarGenT: Generated file ./examples/flatten_pairs.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/flatten_pairs.ml" exited with code 0 - t=0.018s ok + t=0.024s ok InvarGenT:7:InvarGenT:9:flatten_quadrs ... InvarGenT: Generated file ./examples/flatten_quadrs.gadti InvarGenT: Generated file ./examples/flatten_quadrs.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/flatten_quadrs.ml" exited with code 0 - t=0.068s ok -InvarGenT:7:InvarGenT:10:equational_reas ... + t=0.072s ok +InvarGenT:7:InvarGenT:10:flatten_septs ... +InvarGenT: Generated file ./examples/flatten_septs.gadti +InvarGenT: Generated file ./examples/flatten_septs.ml +InvarGenT: Command "ocamlc -w -25 -c ./examples/flatten_septs.ml" exited with code 0 + t=0.956s ok +InvarGenT:7:InvarGenT:11:equational_reas ... InvarGenT: Generated file ./examples/equational_reas.gadti InvarGenT: Generated file ./examples/equational_reas.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equational_reas.ml" exited with code 0 - t=1.932s ok -InvarGenT:7:InvarGenT:11:filter ... + t=1.601s ok +InvarGenT:7:InvarGenT:12:filter ... InvarGenT: Generated file ./examples/filter.gadti InvarGenT: Generated file ./examples/filter.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/filter.ml" exited with code 0 - t=0.340s ok -InvarGenT:7:InvarGenT:12:filter_map ... + t=0.302s ok +InvarGenT:7:InvarGenT:13:filter_map ... InvarGenT: Generated file ./examples/filter_map.gadti InvarGenT: Generated file ./examples/filter_map.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/filter_map.ml" exited with code 0 - t=0.479s ok -InvarGenT:7:InvarGenT:13:binary_upper_bound ... + t=0.434s ok +InvarGenT:7:InvarGenT:14:binary_upper_bound ... InvarGenT: Generated file ./examples/binary_upper_bound.gadti InvarGenT: Generated file ./examples/binary_upper_bound.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/binary_upper_bound.ml" exited with code 0 - t=2.426s ok -InvarGenT:7:InvarGenT:14:ex_config_pc ... + t=1.597s ok +InvarGenT:7:InvarGenT:15:ex_config_pc ... InvarGenT: Generated file ./examples/ex_config_pc.gadti InvarGenT: Generated file ./examples/ex_config_pc.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/ex_config_pc.ml" exited with code 0 - t=0.065s ok -InvarGenT:7:InvarGenT:15:mutual_simple_recursion_eval ... + t=0.056s ok +InvarGenT:7:InvarGenT:16:mutual_simple_recursion_eval ... InvarGenT: Generated file ./examples/mutual_simple_recursion_eval.gadti InvarGenT: Generated file ./examples/mutual_simple_recursion_eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/mutual_simple_recursion_eval.ml" exited with code 0 - t=0.172s ok -InvarGenT:7:InvarGenT:16:binomial_heap_nonrec ... + t=0.149s ok +InvarGenT:7:InvarGenT:17:binomial_heap_nonrec ... InvarGenT: Generated file ./examples/binomial_heap_nonrec.gadti InvarGenT: Generated file ./examples/binomial_heap_nonrec.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/binomial_heap_nonrec.ml" exited with code 0 - t=0.028s ok -InvarGenT:7:InvarGenT:17:mutual_recursion_eval ... + t=0.027s ok +InvarGenT:7:InvarGenT:18:mutual_recursion_eval ... InvarGenT: Generated file ./examples/mutual_recursion_eval.gadti InvarGenT: Generated file ./examples/mutual_recursion_eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/mutual_recursion_eval.ml" exited with code 0 - t=1.287s ok -InvarGenT:7:InvarGenT:18:simple eval-annot ... + t=1.089s ok +InvarGenT:7:InvarGenT:19:simple eval-annot ... InvarGenT: Generated file ./examples/simple_eval.gadti InvarGenT: Generated file ./examples/simple_eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/simple_eval.ml" exited with code 0 - t=0.014s ok -InvarGenT:7:InvarGenT:19:eval-annot ... + t=0.021s ok +InvarGenT:7:InvarGenT:20:eval-annot ... InvarGenT: Generated file ./examples/eval.gadti InvarGenT: Generated file ./examples/eval.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/eval.ml" exited with code 0 - t=0.101s ok -InvarGenT:7:InvarGenT:20:equational_reas-annot ... + t=0.100s ok +InvarGenT:7:InvarGenT:21:equational_reas-annot ... InvarGenT: Generated file ./examples/equational_reas.gadti InvarGenT: Generated file ./examples/equational_reas.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/equational_reas.ml" exited with code 0 - t=2.084s ok -InvarGenT:7:InvarGenT:21:mutual_recursion_eval-annot ... + t=1.726s ok +InvarGenT:7:InvarGenT:22:mutual_recursion_eval-annot ... InvarGenT: Generated file ./examples/mutual_recursion_eval_docs.gadti InvarGenT: Generated file ./examples/mutual_recursion_eval_docs.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/mutual_recursion_eval_docs.ml" exited with code 0 - t=1.292s ok -InvarGenT:7:InvarGenT:22:concat_strings-export ... + t=1.034s ok +InvarGenT:7:InvarGenT:23:concat_strings-export ... InvarGenT: Generated file ./examples/concat_strings.gadti InvarGenT: Generated file ./examples/concat_strings.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/concat_strings.ml" exited with code 0 - t=0.006s ok -InvarGenT:7:InvarGenT:23:list-head ... + t=0.008s ok +InvarGenT:7:InvarGenT:24:list-head ... InvarGenT: Generated file ./examples/list_head.gadti InvarGenT: Generated file ./examples/list_head.ml File "./examples/list_head.ml", line 7, characters 2-27: @@ -389,92 +414,92 @@ Here is an example of a value that is not matched: LNil InvarGenT: Command "ocamlc -w -25 -c ./examples/list_head.ml" exited with code 0 t=0.005s ok -InvarGenT:7:InvarGenT:24:pointwise-head ... +InvarGenT:7:InvarGenT:25:pointwise-head ... TODO -InvarGenT:7:InvarGenT:25:pointwise-refine ... +InvarGenT:7:InvarGenT:26:pointwise-refine ... InvarGenT: Generated file ./examples/pointwise_refine.gadti InvarGenT: Generated file ./examples/pointwise_refine.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_refine.ml" exited with code 0 - t=0.006s ok -InvarGenT:7:InvarGenT:26:pointwise-rbtree_rotate ... + t=0.014s ok +InvarGenT:7:InvarGenT:27:pointwise-rbtree_rotate ... InvarGenT: Generated file ./examples/pointwise_rbtree_rotate.gadti InvarGenT: Generated file ./examples/pointwise_rbtree_rotate.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_rbtree_rotate.ml" exited with code 0 - t=0.026s ok -InvarGenT:7:InvarGenT:27:pointwise-zip2-simpler1 ... + t=0.031s ok +InvarGenT:7:InvarGenT:28:pointwise-zip2-simpler1 ... InvarGenT: Generated file ./examples/pointwise_zip2_simpler1.gadti InvarGenT: Generated file ./examples/pointwise_zip2_simpler1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_zip2_simpler1.ml" exited with code 0 - t=0.013s ok -InvarGenT:7:InvarGenT:28:pointwise-zip2-simpler2 ... + t=0.014s ok +InvarGenT:7:InvarGenT:29:pointwise-zip2-simpler2 ... InvarGenT: Generated file ./examples/pointwise_zip2_simpler2.gadti InvarGenT: Generated file ./examples/pointwise_zip2_simpler2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_zip2_simpler2.ml" exited with code 0 - t=0.038s ok -InvarGenT:7:InvarGenT:29:pointwise-zip2-simpler3 ... + t=0.039s ok +InvarGenT:7:InvarGenT:30:pointwise-zip2-simpler3 ... InvarGenT: Generated file ./examples/pointwise_zip2_simpler3.gadti InvarGenT: Generated file ./examples/pointwise_zip2_simpler3.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_zip2_simpler3.ml" exited with code 0 - t=0.008s ok -InvarGenT:7:InvarGenT:30:pointwise-zip2-simpler4 ... + t=0.006s ok +InvarGenT:7:InvarGenT:31:pointwise-zip2-simpler4 ... InvarGenT: Generated file ./examples/pointwise_zip2_simpler4.gadti InvarGenT: Generated file ./examples/pointwise_zip2_simpler4.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_zip2_simpler4.ml" exited with code 0 - t=0.196s ok -InvarGenT:7:InvarGenT:31:pointwise-zip2 ... + t=0.187s ok +InvarGenT:7:InvarGenT:32:pointwise-zip2 ... InvarGenT: Generated file ./examples/pointwise_zip2.gadti InvarGenT: Generated file ./examples/pointwise_zip2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_zip2.ml" exited with code 0 - t=0.292s ok -InvarGenT:7:InvarGenT:32:pointwise-zip2-harder ... + t=0.282s ok +InvarGenT:7:InvarGenT:33:pointwise-zip2-harder ... InvarGenT: Generated file ./examples/pointwise_zip2_harder.gadti - t=0.276s ok -InvarGenT:7:InvarGenT:33:pointwise-avl_rotl ... + t=0.248s ok +InvarGenT:7:InvarGenT:34:pointwise-avl_rotl ... InvarGenT: Generated file ./examples/pointwise_avl_rotl.gadti InvarGenT: Generated file ./examples/pointwise_avl_rotl.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_avl_rotl.ml" exited with code 0 t=0.034s ok -InvarGenT:7:InvarGenT:34:pointwise-avl_ins ... +InvarGenT:7:InvarGenT:35:pointwise-avl_ins ... InvarGenT: Generated file ./examples/pointwise_avl_ins.gadti InvarGenT: Generated file ./examples/pointwise_avl_ins.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_avl_ins.ml" exited with code 0 - t=0.848s ok -InvarGenT:7:InvarGenT:35:pointwise-extract0 ... + t=0.802s ok +InvarGenT:7:InvarGenT:36:pointwise-extract0 ... InvarGenT: Generated file ./examples/pointwise_extract0.gadti InvarGenT: Generated file ./examples/pointwise_extract0.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_extract0.ml" exited with code 0 - t=0.020s ok -InvarGenT:7:InvarGenT:36:pointwise-extract1 ... + t=0.026s ok +InvarGenT:7:InvarGenT:37:pointwise-extract1 ... InvarGenT: Generated file ./examples/pointwise_extract1.gadti InvarGenT: Generated file ./examples/pointwise_extract1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_extract1.ml" exited with code 0 - t=0.572s ok -InvarGenT:7:InvarGenT:37:pointwise-extract2 ... + t=0.555s ok +InvarGenT:7:InvarGenT:38:pointwise-extract2 ... InvarGenT: Generated file ./examples/pointwise_extract2.gadti InvarGenT: Generated file ./examples/pointwise_extract2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_extract2.ml" exited with code 0 - t=0.342s ok -InvarGenT:7:InvarGenT:38:pointwise-extract ... + t=0.300s ok +InvarGenT:7:InvarGenT:39:pointwise-extract ... InvarGenT: Generated file ./examples/pointwise_extract.gadti InvarGenT: Generated file ./examples/pointwise_extract.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_extract.ml" exited with code 0 - t=0.429s ok -InvarGenT:7:InvarGenT:39:pointwise-run_state ... + t=0.386s ok +InvarGenT:7:InvarGenT:40:pointwise-run_state ... InvarGenT: Generated file ./examples/pointwise_run_state.gadti InvarGenT: Generated file ./examples/pointwise_run_state.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/pointwise_run_state.ml" exited with code 0 - t=0.023s ok -InvarGenT:7:InvarGenT:40:non_outsidein-rx ... + t=0.024s ok +InvarGenT:7:InvarGenT:41:non_outsidein-rx ... InvarGenT: Generated file ./examples/non_outsidein_rx.gadti InvarGenT: Generated file ./examples/non_outsidein_rx.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_outsidein_rx.ml" exited with code 0 - t=0.002s ok -InvarGenT:7:InvarGenT:41:non_pointwise-split ... + t=0.003s ok +InvarGenT:7:InvarGenT:42:non_pointwise-split ... InvarGenT: Generated file ./examples/non_pointwise_split.gadti InvarGenT: Generated file ./examples/non_pointwise_split.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_split.ml" exited with code 0 - t=0.004s ok -InvarGenT:7:InvarGenT:42:non_pointwise-avl_small_rec ... + t=0.008s ok +InvarGenT:7:InvarGenT:43:non_pointwise-avl_small_rec ... InvarGenT: Generated file ./examples/non_pointwise_avl_small_rec.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_small_rec.ml File "./examples/non_pointwise_avl_small_rec.ml", line 20, characters 11-111: @@ -482,8 +507,8 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Node (Less, _, _, _) InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_small_rec.ml" exited with code 0 - t=0.015s ok -InvarGenT:7:InvarGenT:43:non_pointwise-avl_small ... + t=0.013s ok +InvarGenT:7:InvarGenT:44:non_pointwise-avl_small ... InvarGenT: Generated file ./examples/non_pointwise_avl_small.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_small.ml File "./examples/non_pointwise_avl_small.ml", line 21, characters 11-111: @@ -491,8 +516,8 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Node (Less, _, _, _) InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_small.ml" exited with code 0 - t=0.014s ok -InvarGenT:7:InvarGenT:44:non_pointwise-avl_rotr ... + t=0.017s ok +InvarGenT:7:InvarGenT:45:non_pointwise-avl_rotr ... InvarGenT: Generated file ./examples/non_pointwise_avl.gadti InvarGenT: Generated file ./examples/non_pointwise_avl.ml File "./examples/non_pointwise_avl.ml", line 22, characters 4-616: @@ -500,75 +525,75 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Node (More, _, _, Leaf) InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl.ml" exited with code 0 - t=0.134s ok -InvarGenT:7:InvarGenT:45:avl_delmin-simpler ... + t=0.124s ok +InvarGenT:7:InvarGenT:46:avl_delmin-simpler ... InvarGenT: Generated file ./examples/avl_delmin_simpler.gadti InvarGenT: Generated file ./examples/avl_delmin_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/avl_delmin_simpler.ml" exited with code 0 - t=0.217s ok -InvarGenT:7:InvarGenT:46:non_pointwise-avl_delmin-modified ... + t=0.194s ok +InvarGenT:7:InvarGenT:47:non_pointwise-avl_delmin-modified ... InvarGenT: Generated file ./examples/non_pointwise_avl_delmin_modified.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_delmin_modified.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_delmin_modified.ml" exited with code 0 - t=0.328s ok -InvarGenT:7:InvarGenT:47:non_pointwise-avl_delmin ... + t=0.304s ok +InvarGenT:7:InvarGenT:48:non_pointwise-avl_delmin ... InvarGenT: Generated file ./examples/non_pointwise_avl_delmin.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_delmin.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_delmin.ml" exited with code 0 - t=0.574s ok -InvarGenT:7:InvarGenT:48:non_pointwise-avl_delmin2 ... + t=0.503s ok +InvarGenT:7:InvarGenT:49:non_pointwise-avl_delmin2 ... InvarGenT: Generated file ./examples/non_pointwise_avl_delmin2.gadti InvarGenT: Generated file ./examples/non_pointwise_avl_delmin2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_avl_delmin2.ml" exited with code 0 - t=0.585s ok -InvarGenT:7:InvarGenT:49:non_pointwise-fd_comp ... + t=0.481s ok +InvarGenT:7:InvarGenT:50:non_pointwise-fd_comp ... InvarGenT: Generated file ./examples/non_pointwise_fd_comp.gadti InvarGenT: Generated file ./examples/non_pointwise_fd_comp.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_fd_comp.ml" exited with code 0 - t=0.574s ok -InvarGenT:7:InvarGenT:50:non_pointwise-fd_comp2 ... + t=0.552s ok +InvarGenT:7:InvarGenT:51:non_pointwise-fd_comp2 ... InvarGenT: Generated file ./examples/non_pointwise_fd_comp2.gadti InvarGenT: Generated file ./examples/non_pointwise_fd_comp2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_fd_comp2.ml" exited with code 0 - t=0.120s ok -InvarGenT:7:InvarGenT:51:non_pointwise-fd_comp-harder ... + t=0.117s ok +InvarGenT:7:InvarGenT:52:non_pointwise-fd_comp-harder ... TODO -InvarGenT:7:InvarGenT:52:non_pointwise-zip1-simpler ... +InvarGenT:7:InvarGenT:53:non_pointwise-zip1-simpler ... InvarGenT: Generated file ./examples/non_pointwise_zip1_simpler.gadti InvarGenT: Generated file ./examples/non_pointwise_zip1_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_zip1_simpler.ml" exited with code 0 - t=0.028s ok -InvarGenT:7:InvarGenT:53:non_pointwise-zip1-simpler2 ... + t=0.053s ok +InvarGenT:7:InvarGenT:54:non_pointwise-zip1-simpler2 ... InvarGenT: Generated file ./examples/non_pointwise_zip1_simpler2.gadti InvarGenT: Generated file ./examples/non_pointwise_zip1_simpler2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_zip1_simpler2.ml" exited with code 0 - t=0.030s ok -InvarGenT:7:InvarGenT:54:non_pointwise-zip1-modified ... + t=0.051s ok +InvarGenT:7:InvarGenT:55:non_pointwise-zip1-modified ... InvarGenT: Generated file ./examples/non_pointwise_zip1_modified.gadti InvarGenT: Generated file ./examples/non_pointwise_zip1_modified.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_zip1_modified.ml" exited with code 0 - t=0.057s ok -InvarGenT:7:InvarGenT:55:non_pointwise-zip1 ... + t=0.080s ok +InvarGenT:7:InvarGenT:56:non_pointwise-zip1 ... InvarGenT: Generated file ./examples/non_pointwise_zip1.gadti InvarGenT: Generated file ./examples/non_pointwise_zip1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_zip1.ml" exited with code 0 - t=0.119s ok -InvarGenT:7:InvarGenT:56:non_pointwise-leq ... + t=0.145s ok +InvarGenT:7:InvarGenT:57:non_pointwise-leq ... InvarGenT: Generated file ./examples/non_pointwise_leq.gadti InvarGenT: Generated file ./examples/non_pointwise_leq.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_leq.ml" exited with code 0 - t=0.006s ok -InvarGenT:7:InvarGenT:57:non_pointwise-run_state ... + t=0.007s ok +InvarGenT:7:InvarGenT:58:non_pointwise-run_state ... InvarGenT: Generated file ./examples/non_pointwise_run_state.gadti InvarGenT: Generated file ./examples/non_pointwise_run_state.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_run_state.ml" exited with code 0 - t=0.050s ok -InvarGenT:7:InvarGenT:58:non_pointwise-run_state2 ... + t=0.056s ok +InvarGenT:7:InvarGenT:59:non_pointwise-run_state2 ... InvarGenT: Generated file ./examples/non_pointwise_run_state2.gadti InvarGenT: Generated file ./examples/non_pointwise_run_state2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/non_pointwise_run_state2.ml" exited with code 0 - t=0.039s ok -InvarGenT:7:InvarGenT:59:avl_tree ... + t=0.045s ok +InvarGenT:7:InvarGenT:60:avl_tree ... InvarGenT: Generated file ./examples/avl_tree.gadti InvarGenT: Generated file ./examples/avl_tree.ml File "./examples/avl_tree.ml", line 43, characters 4-161: @@ -596,364 +621,364 @@ Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: Empty InvarGenT: Command "ocamlc -w -25 -c ./examples/avl_tree.ml" exited with code 0 - t=9.765s ok -InvarGenT:7:InvarGenT:60:binomial_heap ... + t=7.865s ok +InvarGenT:7:InvarGenT:61:binomial_heap ... TODO -InvarGenT:7:InvarGenT:61:liquid_dotprod-simpler ... +InvarGenT:7:InvarGenT:62:liquid_dotprod-simpler ... InvarGenT: Generated file ./examples/liquid_dotprod_simpler.gadti InvarGenT: Generated file ./examples/liquid_dotprod_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_dotprod_simpler.ml" exited with code 0 - t=0.025s ok -InvarGenT:7:InvarGenT:62:liquid_dotprod ... + t=0.026s ok +InvarGenT:7:InvarGenT:63:liquid_dotprod ... InvarGenT: Generated file ./examples/liquid_dotprod.gadti InvarGenT: Generated file ./examples/liquid_dotprod.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_dotprod.ml" exited with code 0 - t=0.057s ok -InvarGenT:7:InvarGenT:63:liquid_bcopy-simpler ... + t=0.059s ok +InvarGenT:7:InvarGenT:64:liquid_bcopy-simpler ... InvarGenT: Generated file ./examples/liquid_bcopy_simpler.gadti InvarGenT: Generated file ./examples/liquid_bcopy_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bcopy_simpler.ml" exited with code 0 - t=0.032s ok -InvarGenT:7:InvarGenT:64:liquid_bcopy ... + t=0.029s ok +InvarGenT:7:InvarGenT:65:liquid_bcopy ... InvarGenT: Generated file ./examples/liquid_bcopy.gadti InvarGenT: Generated file ./examples/liquid_bcopy.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bcopy.ml" exited with code 0 - t=0.043s ok -InvarGenT:7:InvarGenT:65:liquid_bsearch-simpler ... + t=0.041s ok +InvarGenT:7:InvarGenT:66:liquid_bsearch-simpler ... InvarGenT: Generated file ./examples/liquid_bsearch_simpler.gadti InvarGenT: Generated file ./examples/liquid_bsearch_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch_simpler.ml" exited with code 0 - t=0.111s ok -InvarGenT:7:InvarGenT:66:liquid_bsearch ... + t=0.103s ok +InvarGenT:7:InvarGenT:67:liquid_bsearch ... InvarGenT: Generated file ./examples/liquid_bsearch.gadti InvarGenT: Generated file ./examples/liquid_bsearch.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch.ml" exited with code 0 - t=0.061s ok -InvarGenT:7:InvarGenT:67:liquid_bsearch-harder ... + t=0.065s ok +InvarGenT:7:InvarGenT:68:liquid_bsearch-harder ... InvarGenT: Generated file ./examples/liquid_bsearch_harder.gadti InvarGenT: Generated file ./examples/liquid_bsearch_harder.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch_harder.ml" exited with code 0 t=0.108s ok -InvarGenT:7:InvarGenT:68:liquid_bsearch2-simpler ... +InvarGenT:7:InvarGenT:69:liquid_bsearch2-simpler ... InvarGenT: Generated file ./examples/liquid_bsearch2_simpler.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2_simpler.ml" exited with code 0 - t=1.118s ok -InvarGenT:7:InvarGenT:69:liquid_bsearch2-simpler2 ... + t=0.978s ok +InvarGenT:7:InvarGenT:70:liquid_bsearch2-simpler2 ... InvarGenT: Generated file ./examples/liquid_bsearch2_simpler2.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_simpler2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2_simpler2.ml" exited with code 0 - t=0.005s ok -InvarGenT:7:InvarGenT:70:liquid_bsearch2 ... + t=0.006s ok +InvarGenT:7:InvarGenT:71:liquid_bsearch2 ... InvarGenT: Generated file ./examples/liquid_bsearch2.gadti InvarGenT: Generated file ./examples/liquid_bsearch2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2.ml" exited with code 0 - t=1.004s ok -InvarGenT:7:InvarGenT:71:liquid_bsearch2-harder1 ... + t=0.890s ok +InvarGenT:7:InvarGenT:72:liquid_bsearch2-harder1 ... InvarGenT: Generated file ./examples/liquid_bsearch2_harder1.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_harder1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2_harder1.ml" exited with code 0 - t=0.998s ok -InvarGenT:7:InvarGenT:72:liquid_bsearch2-harder2 ... + t=0.911s ok +InvarGenT:7:InvarGenT:73:liquid_bsearch2-harder2 ... InvarGenT: Generated file ./examples/liquid_bsearch2_harder2.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_harder2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2_harder2.ml" exited with code 0 - t=1.656s ok -InvarGenT:7:InvarGenT:73:liquid_bsearch2-harder3 ... + t=1.442s ok +InvarGenT:7:InvarGenT:74:liquid_bsearch2-harder3 ... InvarGenT: Generated file ./examples/liquid_bsearch2_harder3.gadti InvarGenT: Generated file ./examples/liquid_bsearch2_harder3.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_bsearch2_harder3.ml" exited with code 0 - t=2.364s ok -InvarGenT:7:InvarGenT:74:liquid_bsearch2-harder4 ... + t=1.904s ok +InvarGenT:7:InvarGenT:75:liquid_bsearch2-harder4 ... TODO -InvarGenT:7:InvarGenT:75:liquid_queen-simpler ... +InvarGenT:7:InvarGenT:76:liquid_queen-simpler ... InvarGenT: Generated file ./examples/liquid_queen_simpler.gadti InvarGenT: Generated file ./examples/liquid_queen_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_queen_simpler.ml" exited with code 0 - t=0.211s ok -InvarGenT:7:InvarGenT:76:liquid_queen ... + t=0.198s ok +InvarGenT:7:InvarGenT:77:liquid_queen ... InvarGenT: Generated file ./examples/liquid_queen.gadti InvarGenT: Generated file ./examples/liquid_queen.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_queen.ml" exited with code 0 - t=0.559s ok -InvarGenT:7:InvarGenT:77:liquid_isort-simpler1 ... + t=0.512s ok +InvarGenT:7:InvarGenT:78:liquid_isort-simpler1 ... InvarGenT: Generated file ./examples/liquid_isort_simpler1.gadti InvarGenT: Generated file ./examples/liquid_isort_simpler1.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_simpler1.ml" exited with code 0 - t=0.121s ok -InvarGenT:7:InvarGenT:78:liquid_isort-simpler2 ... + t=0.109s ok +InvarGenT:7:InvarGenT:79:liquid_isort-simpler2 ... InvarGenT: Generated file ./examples/liquid_isort_simpler2.gadti InvarGenT: Generated file ./examples/liquid_isort_simpler2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_simpler2.ml" exited with code 0 - t=0.366s ok -InvarGenT:7:InvarGenT:79:liquid_isort-simpler3 ... + t=0.346s ok +InvarGenT:7:InvarGenT:80:liquid_isort-simpler3 ... InvarGenT: Generated file ./examples/liquid_isort_simpler3.gadti InvarGenT: Generated file ./examples/liquid_isort_simpler3.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_simpler3.ml" exited with code 0 - t=0.181s ok -InvarGenT:7:InvarGenT:80:liquid_isort-simpler ... + t=0.169s ok +InvarGenT:7:InvarGenT:81:liquid_isort-simpler ... InvarGenT: Generated file ./examples/liquid_isort_simpler.gadti InvarGenT: Generated file ./examples/liquid_isort_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_simpler.ml" exited with code 0 - t=0.198s ok -InvarGenT:7:InvarGenT:81:liquid_isort ... + t=0.176s ok +InvarGenT:7:InvarGenT:82:liquid_isort ... InvarGenT: Generated file ./examples/liquid_isort.gadti InvarGenT: Generated file ./examples/liquid_isort.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort.ml" exited with code 0 - t=0.396s ok -InvarGenT:7:InvarGenT:82:liquid_isort-harder ... + t=0.380s ok +InvarGenT:7:InvarGenT:83:liquid_isort-harder ... InvarGenT: Generated file ./examples/liquid_isort_harder.gadti InvarGenT: Generated file ./examples/liquid_isort_harder.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_harder.ml" exited with code 0 - t=0.522s ok -InvarGenT:7:InvarGenT:83:liquid_vecswap_simpler ... + t=0.474s ok +InvarGenT:7:InvarGenT:84:liquid_vecswap_simpler ... InvarGenT: Generated file ./examples/liquid_vecswap_simpler.gadti InvarGenT: Generated file ./examples/liquid_vecswap_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_vecswap_simpler.ml" exited with code 0 - t=0.372s ok -InvarGenT:7:InvarGenT:84:liquid_vecswap ... + t=0.332s ok +InvarGenT:7:InvarGenT:85:liquid_vecswap ... InvarGenT: Generated file ./examples/liquid_vecswap.gadti InvarGenT: Generated file ./examples/liquid_vecswap.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_vecswap.ml" exited with code 0 - t=0.352s ok -InvarGenT:7:InvarGenT:85:liquid_isort-full ... + t=0.323s ok +InvarGenT:7:InvarGenT:86:liquid_isort-full ... InvarGenT: Generated file ./examples/liquid_isort_full.gadti InvarGenT: Generated file ./examples/liquid_isort_full.ml File "./examples/liquid_isort_full.ml", line 35, characters 12-19: Warning 26: unused variable vecswap. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_isort_full.ml" exited with code 0 - t=1.475s ok -InvarGenT:7:InvarGenT:86:liquid_tower_showposts ... + t=1.307s ok +InvarGenT:7:InvarGenT:87:liquid_tower_showposts ... InvarGenT: Generated file ./examples/liquid_tower_showposts.gadti InvarGenT: Generated file ./examples/liquid_tower_showposts.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower_showposts.ml" exited with code 0 - t=0.063s ok -InvarGenT:7:InvarGenT:87:liquid_tower_simpler ... + t=0.056s ok +InvarGenT:7:InvarGenT:88:liquid_tower_simpler ... InvarGenT: Generated file ./examples/liquid_tower_simpler.gadti InvarGenT: Generated file ./examples/liquid_tower_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower_simpler.ml" exited with code 0 - t=0.681s ok -InvarGenT:7:InvarGenT:88:liquid_tower_asserted ... + t=0.673s ok +InvarGenT:7:InvarGenT:89:liquid_tower_asserted ... InvarGenT: Generated file ./examples/liquid_tower_asserted.gadti InvarGenT: Generated file ./examples/liquid_tower_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower_asserted.ml" exited with code 0 - t=4.903s ok -InvarGenT:7:InvarGenT:89:liquid_tower ... + t=4.664s ok +InvarGenT:7:InvarGenT:90:liquid_tower ... InvarGenT: Generated file ./examples/liquid_tower.gadti InvarGenT: Generated file ./examples/liquid_tower.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower.ml" exited with code 0 - t=1.324s ok -InvarGenT:7:InvarGenT:90:liquid_tower_harder ... + t=1.139s ok +InvarGenT:7:InvarGenT:91:liquid_tower_harder ... InvarGenT: Generated file ./examples/liquid_tower_harder.gadti InvarGenT: Generated file ./examples/liquid_tower_harder.ml File "./examples/liquid_tower_harder.ml", line 69, characters 8-10: Warning 26: unused variable sz. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_tower_harder.ml" exited with code 0 - t=7.112s ok -InvarGenT:7:InvarGenT:91:liquid_matmult ... + t=7.125s ok +InvarGenT:7:InvarGenT:92:liquid_matmult ... InvarGenT: Generated file ./examples/liquid_matmult.gadti InvarGenT: Generated file ./examples/liquid_matmult.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_matmult.ml" exited with code 0 - t=0.463s ok -InvarGenT:7:InvarGenT:92:liquid_heapsort-heapify-simpler ... + t=0.384s ok +InvarGenT:7:InvarGenT:93:liquid_heapsort-heapify-simpler ... InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapify_simpler.ml" exited with code 0 - t=3.508s ok -InvarGenT:7:InvarGenT:93:liquid_heapsort-heapify-simpler2 ... + t=2.673s ok +InvarGenT:7:InvarGenT:94:liquid_heapsort-heapify-simpler2 ... InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler2.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapify_simpler2.ml" exited with code 0 - t=9.792s ok -InvarGenT:7:InvarGenT:94:liquid_heapsort-heapify-simpler3 ... + t=6.988s ok +InvarGenT:7:InvarGenT:95:liquid_heapsort-heapify-simpler3 ... InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler3.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapify_simpler3.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapify_simpler3.ml" exited with code 0 - t=5.383s ok -InvarGenT:7:InvarGenT:95:liquid_heapsort-heapify ... + t=3.741s ok +InvarGenT:7:InvarGenT:96:liquid_heapsort-heapify ... InvarGenT: Generated file ./examples/liquid_heapsort_heapify.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapify.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapify.ml" exited with code 0 - t=3.718s ok -InvarGenT:7:InvarGenT:96:liquid_heapsort-heapsort-simpler ... + t=2.752s ok +InvarGenT:7:InvarGenT:97:liquid_heapsort-heapsort-simpler ... InvarGenT: Generated file ./examples/liquid_heapsort_heapsort_simpler.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapsort_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapsort_simpler.ml" exited with code 0 - t=0.074s ok -InvarGenT:7:InvarGenT:97:liquid_heapsort-heapsort ... + t=0.060s ok +InvarGenT:7:InvarGenT:98:liquid_heapsort-heapsort ... InvarGenT: Generated file ./examples/liquid_heapsort_heapsort.gadti InvarGenT: Generated file ./examples/liquid_heapsort_heapsort.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort_heapsort.ml" exited with code 0 - t=0.092s ok -InvarGenT:7:InvarGenT:98:liquid_heapsort ... + t=0.082s ok +InvarGenT:7:InvarGenT:99:liquid_heapsort ... InvarGenT: Generated file ./examples/liquid_heapsort.gadti InvarGenT: Generated file ./examples/liquid_heapsort.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_heapsort.ml" exited with code 0 - t=3.833s ok -InvarGenT:7:InvarGenT:99:liquid_simplex_step_2 ... + t=2.939s ok +InvarGenT:7:InvarGenT:100:liquid_simplex_step_2 ... InvarGenT: Generated file ./examples/liquid_simplex_step_2.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_2.ml" exited with code 0 t=0.255s ok -InvarGenT:7:InvarGenT:100:liquid_simplex_step_2a ... +InvarGenT:7:InvarGenT:101:liquid_simplex_step_2a ... InvarGenT: Generated file ./examples/liquid_simplex_step_2a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_2a.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_2a.ml" exited with code 0 - t=0.217s ok -InvarGenT:7:InvarGenT:101:liquid_simplex_step_3 ... + t=0.199s ok +InvarGenT:7:InvarGenT:102:liquid_simplex_step_3 ... TODO -InvarGenT:7:InvarGenT:102:liquid_simplex_step_3a ... +InvarGenT:7:InvarGenT:103:liquid_simplex_step_3a ... InvarGenT: Generated file ./examples/liquid_simplex_step_3a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_3a.ml File "./examples/liquid_simplex_step_3a.ml", line 43, characters 8-9: Warning 26: unused variable m. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_3a.ml" exited with code 0 - t=4.478s ok -InvarGenT:7:InvarGenT:103:liquid_simplex_step_4 ... + t=4.280s ok +InvarGenT:7:InvarGenT:104:liquid_simplex_step_4 ... TODO -InvarGenT:7:InvarGenT:104:liquid_simplex_step_4a ... +InvarGenT:7:InvarGenT:105:liquid_simplex_step_4a ... InvarGenT: Generated file ./examples/liquid_simplex_step_4a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_4a.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_4a.ml" exited with code 0 - t=0.728s ok -InvarGenT:7:InvarGenT:105:liquid_simplex_step_5a ... + t=0.616s ok +InvarGenT:7:InvarGenT:106:liquid_simplex_step_5a ... InvarGenT: Generated file ./examples/liquid_simplex_step_5a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_5a.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_5a.ml" exited with code 0 - t=6.706s ok -InvarGenT:7:InvarGenT:106:liquid_simplex_step_6a_1 ... + t=5.400s ok +InvarGenT:7:InvarGenT:107:liquid_simplex_step_6a_1 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6a_1.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6a_1.ml File "./examples/liquid_simplex_step_6a_1.ml", line 59, characters 8-9: Warning 26: unused variable m. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6a_1.ml" exited with code 0 - t=0.614s ok -InvarGenT:7:InvarGenT:107:liquid_simplex_step_6_2 ... + t=0.569s ok +InvarGenT:7:InvarGenT:108:liquid_simplex_step_6_2 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6_2.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6_2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6_2.ml" exited with code 0 - t=0.083s ok -InvarGenT:7:InvarGenT:108:liquid_simplex_step_6a_2 ... + t=0.078s ok +InvarGenT:7:InvarGenT:109:liquid_simplex_step_6a_2 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6a_2.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6a_2.ml File "./examples/liquid_simplex_step_6a_2.ml", line 59, characters 8-9: Warning 26: unused variable m. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6a_2.ml" exited with code 0 - t=1.033s ok -InvarGenT:7:InvarGenT:109:liquid_simplex_step_6_3 ... + t=0.917s ok +InvarGenT:7:InvarGenT:110:liquid_simplex_step_6_3 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6_3.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6_3.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6_3.ml" exited with code 0 - t=0.074s ok -InvarGenT:7:InvarGenT:110:liquid_simplex_step_6a_3 ... + t=0.073s ok +InvarGenT:7:InvarGenT:111:liquid_simplex_step_6a_3 ... InvarGenT: Generated file ./examples/liquid_simplex_step_6a_3.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6a_3.ml File "./examples/liquid_simplex_step_6a_3.ml", line 67, characters 8-9: Warning 26: unused variable n. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6a_3.ml" exited with code 0 - t=0.726s ok -InvarGenT:7:InvarGenT:111:liquid_simplex_step_6a ... + t=0.681s ok +InvarGenT:7:InvarGenT:112:liquid_simplex_step_6a ... InvarGenT: Generated file ./examples/liquid_simplex_step_6a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_6a.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_6a.ml" exited with code 0 - t=2.893s ok -InvarGenT:7:InvarGenT:112:liquid_simplex_step_7a ... + t=2.698s ok +InvarGenT:7:InvarGenT:113:liquid_simplex_step_7a ... InvarGenT: Generated file ./examples/liquid_simplex_step_7a.gadti InvarGenT: Generated file ./examples/liquid_simplex_step_7a.ml File "./examples/liquid_simplex_step_7a.ml", line 65, characters 8-9: Warning 26: unused variable m. InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_step_7a.ml" exited with code 0 - t=0.249s ok -InvarGenT:7:InvarGenT:113:liquid_simplex ... + t=0.217s ok +InvarGenT:7:InvarGenT:114:liquid_simplex ... InvarGenT: Generated file ./examples/liquid_simplex.gadti InvarGenT: Generated file ./examples/liquid_simplex.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex.ml" exited with code 0 - t=18.173s ok -InvarGenT:7:InvarGenT:114:liquid_simplex-harder ... + t=14.051s ok +InvarGenT:7:InvarGenT:115:liquid_simplex-harder ... InvarGenT: Generated file ./examples/liquid_simplex_harder.gadti InvarGenT: Generated file ./examples/liquid_simplex_harder.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_simplex_harder.ml" exited with code 0 - t=80.340s ok -InvarGenT:7:InvarGenT:115:liquid_gauss_rowSwap ... + t=54.652s ok +InvarGenT:7:InvarGenT:116:liquid_gauss_rowSwap ... InvarGenT: Generated file ./examples/liquid_gauss_rowSwap.gadti InvarGenT: Generated file ./examples/liquid_gauss_rowSwap.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_rowSwap.ml" exited with code 0 - t=0.023s ok -InvarGenT:7:InvarGenT:116:liquid_gauss_rowElim ... + t=0.026s ok +InvarGenT:7:InvarGenT:117:liquid_gauss_rowElim ... InvarGenT: Generated file ./examples/liquid_gauss_rowElim.gadti InvarGenT: Generated file ./examples/liquid_gauss_rowElim.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_rowElim.ml" exited with code 0 - t=0.049s ok -InvarGenT:7:InvarGenT:117:liquid_gauss_rowMax ... + t=0.054s ok +InvarGenT:7:InvarGenT:118:liquid_gauss_rowMax ... TODO -InvarGenT:7:InvarGenT:118:liquid_gauss_rowMax_2 ... +InvarGenT:7:InvarGenT:119:liquid_gauss_rowMax_2 ... InvarGenT: Generated file ./examples/liquid_gauss_rowMax_2.gadti InvarGenT: Generated file ./examples/liquid_gauss_rowMax_2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_rowMax_2.ml" exited with code 0 - t=0.719s ok -InvarGenT:7:InvarGenT:119:liquid_gauss_simpler ... + t=0.627s ok +InvarGenT:7:InvarGenT:120:liquid_gauss_simpler ... InvarGenT: Generated file ./examples/liquid_gauss_simpler.gadti InvarGenT: Generated file ./examples/liquid_gauss_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_simpler.ml" exited with code 0 - t=4.692s ok -InvarGenT:7:InvarGenT:120:liquid_gauss_simpler_asserted ... + t=4.085s ok +InvarGenT:7:InvarGenT:121:liquid_gauss_simpler_asserted ... InvarGenT: Generated file ./examples/liquid_gauss_simpler_asserted.gadti InvarGenT: Generated file ./examples/liquid_gauss_simpler_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_simpler_asserted.ml" exited with code 0 - t=2.963s ok -InvarGenT:7:InvarGenT:121:liquid_gauss ... + t=2.423s ok +InvarGenT:7:InvarGenT:122:liquid_gauss ... InvarGenT: Generated file ./examples/liquid_gauss.gadti InvarGenT: Generated file ./examples/liquid_gauss.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss.ml" exited with code 0 - t=4.167s ok -InvarGenT:7:InvarGenT:122:liquid_gauss2 ... + t=3.525s ok +InvarGenT:7:InvarGenT:123:liquid_gauss2 ... InvarGenT: Generated file ./examples/liquid_gauss2.gadti InvarGenT: Generated file ./examples/liquid_gauss2.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss2.ml" exited with code 0 - t=3.967s ok -InvarGenT:7:InvarGenT:123:liquid_gauss_asserted ... + t=3.406s ok +InvarGenT:7:InvarGenT:124:liquid_gauss_asserted ... InvarGenT: Generated file ./examples/liquid_gauss_asserted.gadti InvarGenT: Generated file ./examples/liquid_gauss_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_asserted.ml" exited with code 0 - t=3.110s ok -InvarGenT:7:InvarGenT:124:liquid_gauss_harder_asserted ... + t=2.620s ok +InvarGenT:7:InvarGenT:125:liquid_gauss_harder_asserted ... InvarGenT: Generated file ./examples/liquid_gauss_harder_asserted.gadti InvarGenT: Generated file ./examples/liquid_gauss_harder_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_gauss_harder_asserted.ml" exited with code 0 - t=4.671s ok -InvarGenT:7:InvarGenT:125:liquid_gauss_harder ... + t=3.716s ok +InvarGenT:7:InvarGenT:126:liquid_gauss_harder ... TODO -InvarGenT:7:InvarGenT:126:liquid_fft_ffor ... +InvarGenT:7:InvarGenT:127:liquid_fft_ffor ... InvarGenT: Generated file ./examples/liquid_fft_ffor.gadti InvarGenT: Generated file ./examples/liquid_fft_ffor.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft_ffor.ml" exited with code 0 t=0.037s ok -InvarGenT:7:InvarGenT:127:liquid_fft_simpler ... +InvarGenT:7:InvarGenT:128:liquid_fft_simpler ... InvarGenT: Generated file ./examples/liquid_fft_simpler.gadti InvarGenT: Generated file ./examples/liquid_fft_simpler.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft_simpler.ml" exited with code 0 - t=58.688s ok -InvarGenT:7:InvarGenT:128:liquid_fft ... + t=37.845s ok +InvarGenT:7:InvarGenT:129:liquid_fft ... InvarGenT: Generated file ./examples/liquid_fft.gadti InvarGenT: Generated file ./examples/liquid_fft.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft.ml" exited with code 0 - t=58.492s ok -InvarGenT:7:InvarGenT:129:liquid_fft_tests ... + t=35.530s ok +InvarGenT:7:InvarGenT:130:liquid_fft_tests ... InvarGenT: Generated file ./examples/liquid_fft_tests.gadti InvarGenT: Generated file ./examples/liquid_fft_tests.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft_tests.ml" exited with code 0 - t=8.346s ok -InvarGenT:7:InvarGenT:130:liquid_fft_full ... + t=7.710s ok +InvarGenT:7:InvarGenT:131:liquid_fft_full ... InvarGenT: Generated file ./examples/liquid_fft_full.gadti InvarGenT: Generated file ./examples/liquid_fft_full.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft_full.ml" exited with code 0 - t=68.039s ok -InvarGenT:7:InvarGenT:131:liquid_fft_full_asserted ... + t=45.106s ok +InvarGenT:7:InvarGenT:132:liquid_fft_full_asserted ... InvarGenT: Generated file ./examples/liquid_fft_full_asserted.gadti InvarGenT: Generated file ./examples/liquid_fft_full_asserted.ml InvarGenT: Command "ocamlc -w -25 -c ./examples/liquid_fft_full_asserted.ml" exited with code 0 - t=68.124s ok -Ran: 261 tests in: 569.92 seconds. -FAILED: Cases: 261 Tried: 261 Errors: 0 Failures: 0 Skip:0 Todo:10 + t=44.926s ok +Ran: 262 tests in: 419.38 seconds. +FAILED: Cases: 262 Tried: 262 Errors: 0 Failures: 0 Skip:0 Todo:10 -Compilation finished at Fri Feb 27 04:55:17 +Compilation finished at Tue Mar 3 17:04:20