Build:
- 0
2026-06-24 11:05.49: New job: build msat.0.4.1 (696049d43a5b) 2026-06-24 11:05.49: Waiting for resource in pool day11-builds 2026-06-24 11:17.12: Got resource from pool day11-builds 2026-06-24 11:17.12: [profile full] build msat.0.4.1 2026-06-24 11:17.12: build msat.0.4.1 (696049d43a5b) === DEPENDENCIES (5 transitive) === ocaml.4.14.4 b047fb9251f4 ocaml-base-compiler.4.14.4 d3b7ccb2c6fb ocaml-config.2 2d9c209f5590 ocamlbuild.0.16.1 7e0d6aadb209 ocamlfind.1.9.8 214dd418ac02 === STDOUT === Processing: [default: loading data] [msat.0.4.1: dl] [msat.0.4.1: extract] -> retrieved msat.0.4.1 (https://opam.ocaml.org/cache) [msat: make disable_log] + /usr/bin/make "disable_log" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.4.1) - cd src/util; ln -sf log_dummy.ml log.ml [msat: make lib] + /usr/bin/make "lib" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.4.1) - ocamlbuild -log build.log -use-ocamlfind msat.cma msat.cmxa msat.cmxs - + ocamlfind ocamlc -config - + ocamlfind ocamldep -modules src/util/log.mli > src/util/log.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/log.cmi src/util/log.mli - + ocamlfind ocamldep -modules src/util/log.ml > src/util/log.ml.depends - + ocamlfind ocamldep -modules src/core/formula_intf.ml > src/core/formula_intf.ml.depends - + ocamlfind ocamldep -modules src/core/theory_intf.ml > src/core/theory_intf.ml.depends - + ocamlfind ocamldep -modules src/core/plugin_intf.ml > src/core/plugin_intf.ml.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/plugin_intf.cmo src/core/plugin_intf.ml - + ocamlfind ocamldep -modules src/core/expr_intf.ml > src/core/expr_intf.ml.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/formula_intf.cmo src/core/formula_intf.ml - + ocamlfind ocamldep -modules src/solver/tseitin_intf.ml > src/solver/tseitin_intf.ml.depends - + ocamlfind ocamldep -modules src/core/res_intf.ml > src/core/res_intf.ml.depends - + ocamlfind ocamldep -modules src/core/solver_types.mli > src/core/solver_types.mli.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/expr_intf.cmo src/core/expr_intf.ml - + ocamlfind ocamldep -modules src/core/solver_types_intf.ml > src/core/solver_types_intf.ml.depends - + ocamlfind ocamldep -modules src/util/vec.mli > src/util/vec.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/vec.cmi src/util/vec.mli - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/solver_types_intf.cmo src/core/solver_types_intf.ml - + ocamlfind ocamlc -c -bin-annot -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/solver_types.cmi src/core/solver_types.mli - + ocamlfind ocamldep -modules src/core/solver_intf.ml > src/core/solver_intf.ml.depends - + ocamlfind ocamldep -modules src/core/res.mli > src/core/res.mli.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/res_intf.cmo src/core/res_intf.ml - + ocamlfind ocamlc -c -bin-annot -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/res.cmi src/core/res.mli - + ocamlfind ocamldep -modules src/core/internal.mli > src/core/internal.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/internal.cmi src/core/internal.mli - + ocamlfind ocamldep -modules src/core/internal.ml > src/core/internal.ml.depends - + ocamlfind ocamldep -modules src/util/array_util.ml > src/util/array_util.ml.depends - + ocamlfind ocamldep -modules src/util/iheap.mli > src/util/iheap.mli.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/array_util.cmo src/util/array_util.ml - + ocamlfind ocamlc -c -bin-annot -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/iheap.cmi src/util/iheap.mli - + ocamlfind ocamldep -modules src/core/external.mli > src/core/external.mli.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/solver_intf.cmo src/core/solver_intf.ml - + ocamlfind ocamlc -c -bin-annot -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/external.cmi src/core/external.mli - + ocamlfind ocamldep -modules src/core/external.ml > src/core/external.ml.depends - + ocamlfind ocamldep -modules src/solver/solver.mli > src/solver/solver.mli.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/theory_intf.cmo src/core/theory_intf.ml - + ocamlfind ocamlc -c -bin-annot -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/solver.cmi src/solver/solver.mli - + ocamlfind ocamldep -modules src/solver/solver.ml > src/solver/solver.ml.depends - + ocamlfind ocamldep -modules src/solver/mcsolver.mli > src/solver/mcsolver.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/mcsolver.cmi src/solver/mcsolver.mli - + ocamlfind ocamldep -modules src/solver/mcsolver.ml > src/solver/mcsolver.ml.depends - + ocamlfind ocamldep -modules src/core/solver_types.ml > src/core/solver_types.ml.depends - + ocamlfind ocamldep -modules src/backend/dot.mli > src/backend/dot.mli.depends - + ocamlfind ocamldep -modules src/backend/backend_intf.ml > src/backend/backend_intf.ml.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/backend_intf.cmo src/backend/backend_intf.ml - + ocamlfind ocamlc -c -bin-annot -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dot.cmi src/backend/dot.mli - + ocamlfind ocamldep -modules src/backend/dot.ml > src/backend/dot.ml.depends - + ocamlfind ocamldep -modules src/backend/dedukti.mli > src/backend/dedukti.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dedukti.cmi src/backend/dedukti.mli - + ocamlfind ocamldep -modules src/backend/dedukti.ml > src/backend/dedukti.ml.depends - + ocamlfind ocamldep -modules src/core/res.ml > src/core/res.ml.depends - + ocamlfind ocamldep -modules src/solver/tseitin.mli > src/solver/tseitin.mli.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/tseitin_intf.cmo src/solver/tseitin_intf.ml - + ocamlfind ocamlc -c -bin-annot -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/tseitin.cmi src/solver/tseitin.mli - + ocamlfind ocamldep -modules src/solver/tseitin.ml > src/solver/tseitin.ml.depends - + ocamlfind ocamldep -modules src/example/expr.mli > src/example/expr.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/expr.cmi src/example/expr.mli - + ocamlfind ocamldep -modules src/example/expr.ml > src/example/expr.ml.depends - + ocamlfind ocamldep -modules src/example/cnf.mli > src/example/cnf.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/cnf.cmi src/example/cnf.mli - + ocamlfind ocamldep -modules src/example/cnf.ml > src/example/cnf.ml.depends - + ocamlfind ocamldep -modules src/example/sat.mli > src/example/sat.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/sat.cmi src/example/sat.mli - + ocamlfind ocamldep -modules src/example/sat.ml > src/example/sat.ml.depends - + ocamlfind ocamldep -modules src/example/mcsat.ml > src/example/mcsat.ml.depends - + ocamlfind ocamldep -modules src/example/cc.mli > src/example/cc.mli.depends - + ocamlfind ocamldep -modules src/example/sig.mli > src/example/sig.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/sig.cmi src/example/sig.mli - + ocamlfind ocamlc -c -bin-annot -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/cc.cmi src/example/cc.mli - + ocamlfind ocamldep -modules src/example/cc.ml > src/example/cc.ml.depends - + ocamlfind ocamldep -modules src/example/unionfind.mli > src/example/unionfind.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/unionfind.cmi src/example/unionfind.mli - + ocamlfind ocamldep -modules src/example/smt.mli > src/example/smt.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/smt.cmi src/example/smt.mli - + ocamlfind ocamldep -modules src/example/smt.ml > src/example/smt.ml.depends - + ocamlfind ocamldep -modules src/example/unionfind.ml > src/example/unionfind.ml.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/log.cmo src/util/log.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/internal.cmo src/core/internal.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/internal.cmo src/core/internal.ml - File "src/core/internal.ml", line 605, characters 22-40: - 605 | (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/core/internal.ml", line 607, characters 19-32: - 607 | let blevel = backtrack_lvl !is_uip learnt in - ^^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label is_uip was omitted in the application of this function. - File "src/core/internal.ml", line 778, characters 10-22: - 778 | enqueue_bool a 0 (Bcp clause) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 793, characters 12-24: - 793 | enqueue_bool a lvl (Bcp clause) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 857, characters 10-22: - 857 | enqueue_bool first (decision_level ()) (Bcp c) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 916, characters 4-16: - 916 | enqueue_bool a lvl (Semantic lvl) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 1002, characters 8-20: - 1002 | enqueue_bool atom current_level Decision - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 1005, characters 8-20: - 1005 | enqueue_bool a lvl (Semantic lvl) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 169, characters 6-13: - 169 | let nb_vars () = St.nb_elt () - ^^^^^^^ - Warning 32 [unused-value-declaration]: unused value nb_vars. - File "src/core/internal.ml", line 365, characters 6-19: - 365 | let detach_clause c = - ^^^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value detach_clause. - File "src/core/internal.ml", line 374, characters 6-15: - 374 | let satisfied c = Array_util.exists (fun atom -> atom.is_true) c.atoms - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value satisfied. - File "src/core/internal.ml", line 1065, characters 6-15: - 1065 | let check_vec vec = Vec.iter check_clause vec - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value check_vec. - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/external.cmo src/core/external.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/external.cmo src/core/external.ml - File "src/core/external.ml", line 48, characters 2-25: - 48 | type clause = St.clause - ^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type clause. - File "src/core/external.ml", line 49, characters 2-26: - 49 | type proof = Proof.proof - ^^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type proof. - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/solver.cmo src/solver/solver.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/mcsolver.cmo src/solver/mcsolver.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/solver_types.cmo src/core/solver_types.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dot.cmo src/backend/dot.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dot.cmo src/backend/dot.ml - File "src/backend/dot.ml", line 63, characters 6-11: - 63 | let ttify f c = fun fmt () -> f fmt c - ^^^^^ - Warning 32 [unused-value-declaration]: unused value ttify. - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dedukti.cmo src/backend/dedukti.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dedukti.cmo src/backend/dedukti.ml - File "src/backend/dedukti.ml", line 24, characters 6-17: - 24 | let clause_name c = S.St.(c.name) - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value clause_name. - File "src/backend/dedukti.ml", line 26, characters 6-15: - 26 | let pp_clause fmt c = - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value pp_clause. - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/res.cmo src/core/res.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/res.cmo src/core/res.ml - File "src/core/res.ml", line 24, characters 26-44: - 24 | let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/core/res.ml", line 17, characters 2-37: - 17 | type int_cl = clause * St.atom list - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type int_cl. - File "src/core/res.ml", line 20, characters 2-38: - 20 | exception Resolution_error of string - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - Warning 38 [unused-extension]: unused exception Resolution_error - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/tseitin.cmo src/solver/tseitin.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/tseitin.cmo src/solver/tseitin.ml - File "src/solver/tseitin.ml", line 128, characters 6-11: - 128 | let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) - ^^^^^ - Warning 32 [unused-value-declaration]: unused value @. - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/expr.cmo src/example/expr.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/expr.cmo src/example/expr.ml - File "src/example/expr.ml", line 50, characters 14-32: - 50 | let compare = Pervasives.compare - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/example/expr.ml", line 61, characters 16-34: - 61 | let compare = Pervasives.compare - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/example/expr.ml", line 69, characters 16-34: - 69 | let compare = Pervasives.compare - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/example/expr.ml", line 50, characters 4-11: - 50 | let compare = Pervasives.compare - ^^^^^^^ - Warning 32 [unused-value-declaration]: unused value compare. - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/cnf.cmo src/example/cnf.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/sat.cmo src/example/sat.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/sat.cmo src/example/sat.ml - File "src/example/sat.ml", line 38, characters 26-44: - 38 | let compare (a:int) b = Pervasives.compare a b - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/example/sat.ml", line 73, characters 12-23: - 73 | let clause_name c = St.(c.name) - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value clause_name. - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/mcsat.cmo src/example/mcsat.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/cc.cmo src/example/cc.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/smt.cmo src/example/smt.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/unionfind.cmo src/example/unionfind.ml - + ocamlfind ocamlc -pack -g -bin-annot src/util/log.cmo src/core/formula_intf.cmo src/core/plugin_intf.cmo src/core/theory_intf.cmo src/core/expr_intf.cmo src/solver/tseitin_intf.cmo src/core/solver_types_intf.cmo src/core/solver_types.cmo src/core/res_intf.cmo src/core/res.cmo src/core/solver_intf.cmo src/core/internal.cmo src/core/external.cmo src/solver/solver.cmo src/solver/mcsolver.cmo src/backend/dot.cmo src/backend/dedukti.cmo src/solver/tseitin.cmo src/example/expr.cmo src/example/cnf.cmo src/example/sat.cmo src/example/sig.cmi src/example/unionfind.cmo src/example/cc.cmo src/example/mcsat.cmo src/example/smt.cmo -o src/msat.cmo - + ocamlfind ocamldep -modules src/util/vec.ml > src/util/vec.ml.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/vec.cmo src/util/vec.ml - + ocamlfind ocamldep -modules src/util/iheap.ml > src/util/iheap.ml.depends - + ocamlfind ocamldep -modules src/util/sparse_vec.mli > src/util/sparse_vec.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/sparse_vec.cmi src/util/sparse_vec.mli - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/iheap.cmo src/util/iheap.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/iheap.cmo src/util/iheap.ml - File "src/util/iheap.ml", line 78, characters 4-12: - 78 | let increase cmp s n = - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value increase. - + ocamlfind ocamldep -modules src/util/sparse_vec.ml > src/util/sparse_vec.ml.depends - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/sparse_vec.cmo src/util/sparse_vec.ml - + ocamlfind ocamlc -a -I src/backend -I src/util -I src src/backend/backend_intf.cmo src/util/array_util.cmo src/util/sparse_vec.cmo src/util/vec.cmo src/util/iheap.cmo src/msat.cmo -o src/msat.cma - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/plugin_intf.cmx src/core/plugin_intf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/formula_intf.cmx src/core/formula_intf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/expr_intf.cmx src/core/expr_intf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/vec.cmx src/util/vec.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/solver_types_intf.cmx src/core/solver_types_intf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/solver_types.cmx src/core/solver_types.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/log.cmx src/util/log.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/res_intf.cmx src/core/res_intf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/res.cmx src/core/res.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/res.cmx src/core/res.ml - File "src/core/res.ml", line 24, characters 26-44: - 24 | let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/core/res.ml", line 17, characters 2-37: - 17 | type int_cl = clause * St.atom list - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type int_cl. - File "src/core/res.ml", line 20, characters 2-38: - 20 | exception Resolution_error of string - ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - Warning 38 [unused-extension]: unused exception Resolution_error - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/sparse_vec.cmx src/util/sparse_vec.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/array_util.cmx src/util/array_util.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/iheap.cmx src/util/iheap.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/util -I src -I src/backend -I src/core -I src/solver -I src/example -I src/util/smtlib -o src/util/iheap.cmx src/util/iheap.ml - File "src/util/iheap.ml", line 78, characters 4-12: - 78 | let increase cmp s n = - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value increase. - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/internal.cmx src/core/internal.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/internal.cmx src/core/internal.ml - File "src/core/internal.ml", line 605, characters 22-40: - 605 | (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/core/internal.ml", line 607, characters 19-32: - 607 | let blevel = backtrack_lvl !is_uip learnt in - ^^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label is_uip was omitted in the application of this function. - File "src/core/internal.ml", line 778, characters 10-22: - 778 | enqueue_bool a 0 (Bcp clause) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 793, characters 12-24: - 793 | enqueue_bool a lvl (Bcp clause) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 857, characters 10-22: - 857 | enqueue_bool first (decision_level ()) (Bcp c) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 916, characters 4-16: - 916 | enqueue_bool a lvl (Semantic lvl) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 1002, characters 8-20: - 1002 | enqueue_bool atom current_level Decision - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 1005, characters 8-20: - 1005 | enqueue_bool a lvl (Semantic lvl) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 169, characters 6-13: - 169 | let nb_vars () = St.nb_elt () - ^^^^^^^ - Warning 32 [unused-value-declaration]: unused value nb_vars. - File "src/core/internal.ml", line 365, characters 6-19: - 365 | let detach_clause c = - ^^^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value detach_clause. - File "src/core/internal.ml", line 374, characters 6-15: - 374 | let satisfied c = Array_util.exists (fun atom -> atom.is_true) c.atoms - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value satisfied. - File "src/core/internal.ml", line 1065, characters 6-15: - 1065 | let check_vec vec = Vec.iter check_clause vec - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value check_vec. - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/solver_intf.cmx src/core/solver_intf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/external.cmx src/core/external.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/external.cmx src/core/external.ml - File "src/core/external.ml", line 48, characters 2-25: - 48 | type clause = St.clause - ^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type clause. - File "src/core/external.ml", line 49, characters 2-26: - 49 | type proof = Proof.proof - ^^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type proof. - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/core -I src -I src/backend -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/core/theory_intf.cmx src/core/theory_intf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/backend_intf.cmx src/backend/backend_intf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/tseitin_intf.cmx src/solver/tseitin_intf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/expr.cmx src/example/expr.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/expr.cmx src/example/expr.ml - File "src/example/expr.ml", line 50, characters 14-32: - 50 | let compare = Pervasives.compare - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/example/expr.ml", line 61, characters 16-34: - 61 | let compare = Pervasives.compare - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/example/expr.ml", line 69, characters 16-34: - 69 | let compare = Pervasives.compare - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/example/expr.ml", line 50, characters 4-11: - 50 | let compare = Pervasives.compare - ^^^^^^^ - Warning 32 [unused-value-declaration]: unused value compare. - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/tseitin.cmx src/solver/tseitin.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/tseitin.cmx src/solver/tseitin.ml - File "src/solver/tseitin.ml", line 128, characters 6-11: - 128 | let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) - ^^^^^ - Warning 32 [unused-value-declaration]: unused value @. - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dot.cmx src/backend/dot.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dot.cmx src/backend/dot.ml - File "src/backend/dot.ml", line 63, characters 6-11: - 63 | let ttify f c = fun fmt () -> f fmt c - ^^^^^ - Warning 32 [unused-value-declaration]: unused value ttify. - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/solver.cmx src/solver/solver.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/unionfind.cmx src/example/unionfind.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dedukti.cmx src/backend/dedukti.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/backend -I src -I src/core -I src/solver -I src/util -I src/example -I src/util/smtlib -o src/backend/dedukti.cmx src/backend/dedukti.ml - File "src/backend/dedukti.ml", line 24, characters 6-17: - 24 | let clause_name c = S.St.(c.name) - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value clause_name. - File "src/backend/dedukti.ml", line 26, characters 6-15: - 26 | let pp_clause fmt c = - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value pp_clause. - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/solver -I src -I src/backend -I src/core -I src/util -I src/example -I src/util/smtlib -o src/solver/mcsolver.cmx src/solver/mcsolver.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/cc.cmx src/example/cc.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/cnf.cmx src/example/cnf.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/sat.cmx src/example/sat.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/sat.cmx src/example/sat.ml - File "src/example/sat.ml", line 38, characters 26-44: - 38 | let compare (a:int) b = Pervasives.compare a b - ^^^^^^^^^^^^^^^^^^ - Alert deprecated: module Stdlib.Pervasives - Use Stdlib instead. - - If you need to stay compatible with OCaml < 4.07, you can use the - stdlib-shims library: https://github.com/ocaml/stdlib-shims - File "src/example/sat.ml", line 73, characters 12-23: - 73 | let clause_name c = St.(c.name) - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value clause_name. - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/mcsat.cmx src/example/mcsat.ml - + ocamlfind ocamlopt -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -unbox-closures -for-pack Msat -inline 100 -O3 -unbox-closures-factor 20 -color always -I src/example -I src -I src/backend -I src/core -I src/solver -I src/util -I src/util/smtlib -o src/example/smt.cmx src/example/smt.ml - + touch src/msat.mli ; if ocamlfind ocamlopt -pack -g -bin-annot -I src/util -I src/core -I src/solver -I src/backend -I src/example src/util/log.cmx src/core/formula_intf.cmx src/core/plugin_intf.cmx src/core/theory_intf.cmx src/core/expr_intf.cmx src/solver/tseitin_intf.cmx src/core/solver_types_intf.cmx src/core/solver_types.cmx src/core/res_intf.cmx src/core/res.cmx src/core/solver_intf.cmx src/core/internal.cmx src/core/external.cmx src/solver/solver.cmx src/solver/mcsolver.cmx src/backend/dot.cmx src/backend/dedukti.cmx src/solver/tseitin.cmx src/example/expr.cmx src/example/cnf.cmx src/example/sat.cmx src/example/sig.cmi src/example/unionfind.cmx src/example/cc.cmx src/example/mcsat.cmx src/example/smt.cmx -o src/msat.cmx ; then rm -f src/msat.mli ; else rm -f src/msat.mli ; exit 1; fi - + ocamlfind ocamlopt -a -I src/backend -I src/util -I src src/backend/backend_intf.cmx src/util/array_util.cmx src/util/sparse_vec.cmx src/util/vec.cmx src/util/iheap.cmx src/msat.cmx -o src/msat.cmxa - + ocamlfind ocamlopt -shared -linkall -I src src/msat.cmxa -o src/msat.cmxs -> compiled msat.0.4.1 [msat: make install] + /usr/bin/make "install" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.4.1) - ocamlbuild -log build.log -use-ocamlfind msat.cma msat.cmxa msat.cmxs - + ocamlfind ocamlc -config - ocamlfind install msat META _build/src/msat.cma _build/src/msat.cmxa _build/src/msat.cmxs _build/src/msat.a _build/src/msat.cmi - Installed /home/opam/.opam/default/lib/msat/msat.cmi - Installed /home/opam/.opam/default/lib/msat/msat.a - Installed /home/opam/.opam/default/lib/msat/msat.cmxs - Installed /home/opam/.opam/default/lib/msat/msat.cmxa - Installed /home/opam/.opam/default/lib/msat/msat.cma - Installed /home/opam/.opam/default/lib/msat/META -> installed msat.0.4.1 === STDERR === 2026-06-24 11:17.50: OK: build msat.0.4.1 (runc: 9.6s, disk: 52KB) 2026-06-24 11:17.50: Job succeeded