Build:
- 0
2026-06-24 11:05.49: New job: build msat.0.6 (a8754b720873) 2026-06-24 11:05.49: Waiting for resource in pool day11-builds 2026-06-24 11:15.30: Got resource from pool day11-builds 2026-06-24 11:15.30: [profile full] build msat.0.6 2026-06-24 11:15.30: build msat.0.6 (a8754b720873) === 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.6: dl] [msat.0.6: extract] -> retrieved msat.0.6 (https://opam.ocaml.org/cache) [msat: make disable_log] + /usr/bin/make "disable_log" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.6) - 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.6) - ocamlbuild -log build.log -use-ocamlfind msat.cma msat.cmxa msat.cmxs - + ocamlfind ocamlc -config - + ocamlfind ocamlopt unix.cmxa -I /home/opam/.opam/default/lib/ocamlbuild /home/opam/.opam/default/lib/ocamlbuild/ocamlbuildlib.cmxa -linkpkg myocamlbuild.ml /home/opam/.opam/default/lib/ocamlbuild/ocamlbuild.cmx -o myocamlbuild - + 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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/core/res.ml > src/core/res.ml.depends - + ocamlfind ocamldep -modules src/backend/backend_intf.ml > src/backend/backend_intf.ml.depends - + ocamlfind ocamldep -modules src/backend/dot.mli > src/backend/dot.mli.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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/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/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/sat/sat.mli > src/sat/sat.mli.depends - + ocamlfind ocamlc -c -bin-annot -color always -I src/sat -I src -I src/backend -I src/mcsat -I src/core -I src/smt -I src/solver -I src/util -o src/sat/sat.cmi src/sat/sat.mli - + ocamlfind ocamldep -modules src/sat/sat.ml > src/sat/sat.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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -o src/core/internal.cmo src/core/internal.ml - File "src/core/internal.ml", line 524, characters 6-18: - 524 | enqueue_bool a lvl Semantic - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 801, characters 12-24: - 801 | 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 865, characters 12-24: - 865 | 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 935, characters 8-20: - 935 | enqueue_bool p (decision_level ()) (Bcp c) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 1026, characters 8-20: - 1026 | 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 182, characters 6-13: - 182 | let nb_vars () = St.nb_elt () - ^^^^^^^ - Warning 32 [unused-value-declaration]: unused value nb_vars. - File "src/core/internal.ml", line 394, characters 6-15: - 394 | 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 555, characters 6-19: - 555 | let max_lvl_atoms (l:atom list) : int * atom list = - ^^^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value max_lvl_atoms. - File "src/core/internal.ml", line 1097, characters 6-15: - 1097 | 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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -o src/core/external.cmo src/core/external.ml - File "src/core/external.ml", line 51, characters 2-25: - 51 | type clause = St.clause - ^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type clause. - File "src/core/external.ml", line 52, characters 2-26: - 52 | 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/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/core -I src -I src/backend -I src/mcsat -I src/smt -I src/solver -I src/util -I src/sat -o src/core/solver_types.cmo src/core/solver_types.ml - File "src/core/solver_types.ml", line 19, characters 0-11: - 19 | open Printf - ^^^^^^^^^^^ - Warning 33 [unused-open]: unused open Stdlib.Printf. - + 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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -o src/core/res.cmo src/core/res.ml - File "src/core/res.ml", line 30, characters 26-44: - 30 | 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 - File "src/core/res.ml", line 23, characters 6-11: - 23 | let error = 1 - ^^^^^ - Warning 32 [unused-value-declaration]: unused value error. - File "src/core/res.ml", line 24, characters 6-10: - 24 | let warn = 3 - ^^^^ - Warning 32 [unused-value-declaration]: unused value warn. - + 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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -o src/backend/dot.cmo src/backend/dot.ml - File "src/backend/dot.ml", lines 71-83, characters 4-48: - 71 | ....match S.(n.step) with - 72 | | S.Hypothesis -> - 73 | print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE" - 74 | [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; - 75 | | S.Lemma lemma -> - ... - 80 | print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY" - 81 | [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; - 82 | print_dot_res_node fmt (res_node_id n) a; - 83 | print_edge fmt (node_id n) (res_node_id n) - Warning 8 [partial-match]: this pattern-matching is not exhaustive. - Here is an example of a case that is not matched: - Assumption - File "src/backend/dot.ml", line 68, characters 6-11: - 68 | 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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/solver -I src -I src/backend -I src/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/util -I src/sat -o src/solver/tseitin.cmo src/solver/tseitin.ml - File "src/solver/tseitin.ml", line 130, characters 6-11: - 130 | 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/sat -I src -I src/backend -I src/mcsat -I src/core -I src/smt -I src/solver -I src/util -o src/sat/sat.cmo src/sat/sat.ml - + ocamlfind ocamlc -c -g -bin-annot -safe-string -short-paths -w K -w X -w Y -strict-sequence -color always -I src/sat -I src -I src/backend -I src/mcsat -I src/core -I src/smt -I src/solver -I src/util -o src/sat/sat.cmo src/sat/sat.ml - File "src/sat/sat.ml", line 57, characters 26-44: - 57 | 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/sat/sat.ml", line 49, characters 6-10: - 49 | let sign i = i > 0 - ^^^^ - Warning 32 [unused-value-declaration]: unused value sign. - File "src/sat/sat.ml", line 51, characters 6-16: - 51 | let apply_sign b i = if b then i else neg i - ^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value apply_sign. - File "src/sat/sat.ml", line 53, characters 6-14: - 53 | let set_sign b i = if b then abs i else neg (abs i) - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value set_sign. - File "src/sat/sat.ml", line 57, characters 6-13: - 57 | let compare (a:int) b = Pervasives.compare a b - ^^^^^^^ - Warning 32 [unused-value-declaration]: unused value compare. - + 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/backend_intf.cmo src/backend/dot.cmo src/backend/dedukti.cmo src/solver/tseitin.cmo src/sat/sat.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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -o src/util/sparse_vec.cmo src/util/sparse_vec.ml - + ocamlfind ocamlc -a -I src/util -I src 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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/core -I src -I src/backend -I src/mcsat -I src/smt -I src/solver -I src/util -I src/sat -o src/core/solver_types.cmx src/core/solver_types.ml - File "src/core/solver_types.ml", line 19, characters 0-11: - 19 | open Printf - ^^^^^^^^^^^ - Warning 33 [unused-open]: unused open Stdlib.Printf. - + 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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -o src/core/res.cmx src/core/res.ml - File "src/core/res.ml", line 30, characters 26-44: - 30 | 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 - File "src/core/res.ml", line 23, characters 6-11: - 23 | let error = 1 - ^^^^^ - Warning 32 [unused-value-declaration]: unused value error. - File "src/core/res.ml", line 24, characters 6-10: - 24 | let warn = 3 - ^^^^ - Warning 32 [unused-value-declaration]: unused value warn. - + 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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -o src/core/internal.cmx src/core/internal.ml - File "src/core/internal.ml", line 524, characters 6-18: - 524 | enqueue_bool a lvl Semantic - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 801, characters 12-24: - 801 | 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 865, characters 12-24: - 865 | 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 935, characters 8-20: - 935 | enqueue_bool p (decision_level ()) (Bcp c) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 1026, characters 8-20: - 1026 | 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 182, characters 6-13: - 182 | let nb_vars () = St.nb_elt () - ^^^^^^^ - Warning 32 [unused-value-declaration]: unused value nb_vars. - File "src/core/internal.ml", line 394, characters 6-15: - 394 | 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 555, characters 6-19: - 555 | let max_lvl_atoms (l:atom list) : int * atom list = - ^^^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value max_lvl_atoms. - File "src/core/internal.ml", line 1097, characters 6-15: - 1097 | 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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -o src/core/external.cmx src/core/external.ml - File "src/core/external.ml", line 51, characters 2-25: - 51 | type clause = St.clause - ^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type clause. - File "src/core/external.ml", line 52, characters 2-26: - 52 | 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/mcsat -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/solver -I src -I src/backend -I src/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/solver -I src -I src/backend -I src/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/backend -I src -I src/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -o src/backend/dot.cmx src/backend/dot.ml - File "src/backend/dot.ml", lines 71-83, characters 4-48: - 71 | ....match S.(n.step) with - 72 | | S.Hypothesis -> - 73 | print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE" - 74 | [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; - 75 | | S.Lemma lemma -> - ... - 80 | print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY" - 81 | [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; - 82 | print_dot_res_node fmt (res_node_id n) a; - 83 | print_edge fmt (node_id n) (res_node_id n) - Warning 8 [partial-match]: this pattern-matching is not exhaustive. - Here is an example of a case that is not matched: - Assumption - File "src/backend/dot.ml", line 68, characters 6-11: - 68 | 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/backend -I src -I src/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/util -I src/sat -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/mcsat -I src/core -I src/smt -I src/util -I src/sat -o src/solver/tseitin.cmx src/solver/tseitin.ml - File "src/solver/tseitin.ml", line 130, characters 6-11: - 130 | 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/sat -I src -I src/backend -I src/mcsat -I src/core -I src/smt -I src/solver -I src/util -o src/sat/sat.cmx src/sat/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/sat -I src -I src/backend -I src/mcsat -I src/core -I src/smt -I src/solver -I src/util -o src/sat/sat.cmx src/sat/sat.ml - File "src/sat/sat.ml", line 57, characters 26-44: - 57 | 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/sat/sat.ml", line 49, characters 6-10: - 49 | let sign i = i > 0 - ^^^^ - Warning 32 [unused-value-declaration]: unused value sign. - File "src/sat/sat.ml", line 51, characters 6-16: - 51 | let apply_sign b i = if b then i else neg i - ^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value apply_sign. - File "src/sat/sat.ml", line 53, characters 6-14: - 53 | let set_sign b i = if b then abs i else neg (abs i) - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value set_sign. - File "src/sat/sat.ml", line 57, characters 6-13: - 57 | let compare (a:int) b = Pervasives.compare a b - ^^^^^^^ - Warning 32 [unused-value-declaration]: unused value compare. - + 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/sat 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/backend_intf.cmx src/backend/dot.cmx src/backend/dedukti.cmx src/solver/tseitin.cmx src/sat/sat.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/util -I src 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.6 [msat: make install] + /usr/bin/make "DOCDIR=/home/opam/.opam/default/doc/msat" "install" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.6) - ocamlbuild -log build.log -use-ocamlfind msat.cma msat.cmxa msat.cmxs - + ocamlfind ocamlc -config - + 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 - if [ -d "msat.docdir" ]; then \ - mkdir -p /home/opam/.opam/default/doc/msat ; \ - cp -v msat.docdir/*.html msat.docdir/*.css /home/opam/.opam/default/doc/msat ; \ - fi -> installed msat.0.6 === STDERR === 2026-06-24 11:15.55: OK: build msat.0.6 (runc: 8.1s, disk: 47KB) 2026-06-24 11:15.55: Job succeeded