Build:
- 0
2026-06-16 11:34.41: New job: build msat.0.3 (6a01868f2d01) 2026-06-16 11:34.41: Waiting for resource in pool day11-builds 2026-06-16 11:46.30: Got resource from pool day11-builds 2026-06-16 11:46.30: [profile full] build msat.0.3 2026-06-16 11:46.30: build msat.0.3 (6a01868f2d01) === DEPENDENCIES (5 transitive) === ocaml.4.14.4 cb826ea44eb2 ocaml-base-compiler.4.14.4 d2f775f983d7 ocaml-config.2 669e0fcf9e4d ocamlbuild.0.16.1 8f6c52e6fce8 ocamlfind.1.9.8 6025f4a8e98e === STDOUT === Processing: [default: loading data] [msat.0.3: dl] [msat.0.3: extract] -> retrieved msat.0.3 (https://opam.ocaml.org/cache) [msat: make disable_log] + /usr/bin/make "disable_log" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.3) - cd 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.3) - ocamlbuild -log build.log -use-ocamlfind -classic-display -Is solver,sat,smt,backend,util,util/smtlib msat.cma msat.cmxa msat.cmxs - + ocamlfind ocamlc -config - + ocamlfind ocamldep -modules util/log.mli > util/log.mli.depends - + ocamlfind ocamlc -c -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/log.cmi util/log.mli - + ocamlfind ocamldep -modules util/log.ml > util/log.ml.depends - + ocamlfind ocamldep -modules solver/formula_intf.ml > solver/formula_intf.ml.depends - + ocamlfind ocamldep -modules util/hstring.mli > util/hstring.mli.depends - + ocamlfind ocamldep -modules util/hashcons.mli > util/hashcons.mli.depends - + ocamlfind ocamlc -c -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/hashcons.cmi util/hashcons.mli - + ocamlfind ocamlc -c -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/hstring.cmi util/hstring.mli - + ocamlfind ocamldep -modules solver/theory_intf.ml > solver/theory_intf.ml.depends - + ocamlfind ocamldep -modules solver/plugin_intf.ml > solver/plugin_intf.ml.depends - + ocamlfind ocamldep -modules solver/expr_intf.ml > solver/expr_intf.ml.depends - + ocamlfind ocamldep -modules solver/tseitin_intf.ml > solver/tseitin_intf.ml.depends - + ocamlfind ocamldep -modules solver/res_intf.ml > solver/res_intf.ml.depends - + ocamlfind ocamldep -modules solver/solver_types.mli > solver/solver_types.mli.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/expr_intf.cmo solver/expr_intf.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/formula_intf.cmo solver/formula_intf.ml - + ocamlfind ocamldep -modules solver/solver_types_intf.ml > solver/solver_types_intf.ml.depends - + ocamlfind ocamldep -modules util/either.mli > util/either.mli.depends - + ocamlfind ocamldep -modules util/vec.mli > util/vec.mli.depends - + ocamlfind ocamlc -c -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/either.cmi util/either.mli - + ocamlfind ocamlc -c -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/vec.cmi util/vec.mli - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver_types_intf.cmo solver/solver_types_intf.ml - + ocamlfind ocamlc -c -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver_types.cmi solver/solver_types.mli - + ocamlfind ocamldep -modules solver/solver_intf.ml > solver/solver_intf.ml.depends - + ocamlfind ocamldep -modules solver/res.mli > solver/res.mli.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/res_intf.cmo solver/res_intf.ml - + ocamlfind ocamlc -c -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/res.cmi solver/res.mli - + ocamlfind ocamldep -modules solver/internal.mli > solver/internal.mli.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/plugin_intf.cmo solver/plugin_intf.ml - + ocamlfind ocamlc -c -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/internal.cmi solver/internal.mli - + ocamlfind ocamldep -modules solver/internal.ml > solver/internal.ml.depends - + ocamlfind ocamldep -modules util/iheap.mli > util/iheap.mli.depends - + ocamlfind ocamlc -c -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/iheap.cmi util/iheap.mli - + ocamlfind ocamldep -modules solver/solver.mli > solver/solver.mli.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver_intf.cmo solver/solver_intf.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/theory_intf.cmo solver/theory_intf.ml - + ocamlfind ocamlc -c -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver.cmi solver/solver.mli - + ocamlfind ocamldep -modules solver/solver.ml > solver/solver.ml.depends - + ocamlfind ocamldep -modules solver/mcsolver.mli > solver/mcsolver.mli.depends - + ocamlfind ocamlc -c -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/mcsolver.cmi solver/mcsolver.mli - + ocamlfind ocamldep -modules solver/mcsolver.ml > solver/mcsolver.ml.depends - + ocamlfind ocamldep -modules solver/solver_types.ml > solver/solver_types.ml.depends - + ocamlfind ocamldep -modules backend/dot.mli > backend/dot.mli.depends - + ocamlfind ocamldep -modules backend/backend_intf.ml > backend/backend_intf.ml.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/backend_intf.cmo backend/backend_intf.ml - + ocamlfind ocamlc -c -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dot.cmi backend/dot.mli - + ocamlfind ocamldep -modules backend/dot.ml > backend/dot.ml.depends - + ocamlfind ocamldep -modules backend/dedukti.mli > backend/dedukti.mli.depends - + ocamlfind ocamlc -c -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dedukti.cmi backend/dedukti.mli - + ocamlfind ocamldep -modules backend/dedukti.ml > backend/dedukti.ml.depends - + ocamlfind ocamldep -modules solver/res.ml > solver/res.ml.depends - + ocamlfind ocamldep -modules solver/tseitin.mli > solver/tseitin.mli.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/tseitin_intf.cmo solver/tseitin_intf.ml - + ocamlfind ocamlc -c -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/tseitin.cmi solver/tseitin.mli - + ocamlfind ocamldep -modules solver/tseitin.ml > solver/tseitin.ml.depends - + ocamlfind ocamldep -modules smt/expr.mli > smt/expr.mli.depends - + ocamlfind ocamlc -c -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/expr.cmi smt/expr.mli - + ocamlfind ocamldep -modules smt/expr.ml > smt/expr.ml.depends - + ocamlfind ocamldep -modules smt/cnf.mli > smt/cnf.mli.depends - + ocamlfind ocamlc -c -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/cnf.cmi smt/cnf.mli - + ocamlfind ocamldep -modules smt/cnf.ml > smt/cnf.ml.depends - + ocamlfind ocamldep -modules sat/sat.mli > sat/sat.mli.depends - + ocamlfind ocamlc -c -I sat -I backend -I smt -I solver -I util -I util/smtlib -o sat/sat.cmi sat/sat.mli - + ocamlfind ocamldep -modules sat/sat.ml > sat/sat.ml.depends - + ocamlfind ocamldep -modules smt/mcsat.ml > smt/mcsat.ml.depends - + ocamlfind ocamldep -modules smt/cc.mli > smt/cc.mli.depends - + ocamlfind ocamldep -modules smt/sig.mli > smt/sig.mli.depends - + ocamlfind ocamlc -c -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/sig.cmi smt/sig.mli - + ocamlfind ocamlc -c -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/cc.cmi smt/cc.mli - + ocamlfind ocamldep -modules smt/cc.ml > smt/cc.ml.depends - + ocamlfind ocamldep -modules smt/unionfind.mli > smt/unionfind.mli.depends - + ocamlfind ocamlc -c -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/unionfind.cmi smt/unionfind.mli - + ocamlfind ocamldep -modules smt/smt.mli > smt/smt.mli.depends - + ocamlfind ocamlc -c -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/smt.cmi smt/smt.mli - + ocamlfind ocamldep -modules smt/smt.ml > smt/smt.ml.depends - + ocamlfind ocamldep -modules smt/unionfind.ml > smt/unionfind.ml.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/log.cmo util/log.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/internal.cmo solver/internal.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/internal.cmo solver/internal.ml - File "solver/internal.ml", line 197, characters 57-75: - 197 | module Mi = Map.Make(struct type t = int let compare = Pervasives.compare end) - ^^^^^^^^^^^^^^^^^^ - 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 "solver/internal.ml", line 519, characters 41-59: - 519 | let learnt = List.sort (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in - ^^^^^^^^^^^^^^^^^^ - 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 "solver/internal.ml", line 222, characters 6-14: - 222 | let f_filter i = - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value f_filter. - File "solver/internal.ml", line 278, characters 6-16: - 278 | let nb_learnts () = Vec.size env.clauses_learnt - ^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value nb_learnts. - File "solver/internal.ml", line 855, characters 6-22: - 855 | let remove_satisfied vec = - ^^^^^^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value remove_satisfied. - File "solver/internal.ml", line 954, characters 6-15: - 954 | let check_vec vec = - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value check_vec. - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver.cmo solver/solver.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver.cmo solver/solver.ml - File "solver/solver.ml", line 96, characters 6-17: - 96 | let proof_debug _ = assert false - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value proof_debug. - File "solver/solver.ml", line 116, characters 2-25: - 116 | type clause = St.clause - ^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type clause. - File "solver/solver.ml", line 117, characters 2-26: - 117 | type proof = Proof.proof - ^^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type proof. - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/mcsolver.cmo solver/mcsolver.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver_types.cmo solver/solver_types.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver_types.cmo solver/solver_types.ml - File "solver/solver_types.ml", line 200, characters 6-14: - 200 | let destruct = Either.destruct - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value destruct. - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dot.cmo backend/dot.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dot.cmo backend/dot.ml - File "backend/dot.ml", line 51, characters 6-11: - 51 | let ttify f c = fun fmt () -> f fmt c - ^^^^^ - Warning 32 [unused-value-declaration]: unused value ttify. - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dedukti.cmo backend/dedukti.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dedukti.cmo backend/dedukti.ml - File "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 "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 -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/res.cmo solver/res.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/res.cmo solver/res.ml - File "solver/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 "solver/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 "solver/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 -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/tseitin.cmo solver/tseitin.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/tseitin.cmo solver/tseitin.ml - File "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 -safe-string -short-paths -w K -w X -w Y -strict-sequence -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/expr.cmo smt/expr.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/expr.cmo smt/expr.ml - File "smt/expr.ml", line 48, characters 14-32: - 48 | 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 "smt/expr.ml", line 63, characters 16-34: - 63 | 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 "smt/expr.ml", line 71, characters 16-34: - 71 | 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 - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/cnf.cmo smt/cnf.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I sat -I backend -I smt -I solver -I util -I util/smtlib -o sat/sat.cmo sat/sat.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I sat -I backend -I smt -I solver -I util -I util/smtlib -o sat/sat.cmo sat/sat.ml - File "sat/sat.ml", line 36, characters 26-44: - 36 | 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 "sat/sat.ml", line 75, characters 12-23: - 75 | let clause_name c = St.(c.name) - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value clause_name. - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/mcsat.cmo smt/mcsat.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/cc.cmo smt/cc.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/smt.cmo smt/smt.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/smt.cmo smt/smt.ml - File "smt/smt.ml", line 66, characters 10-21: - 66 | let clause_name c = St.(c.name) - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value clause_name. - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/unionfind.cmo smt/unionfind.ml - + ocamlfind ocamlc -pack -g util/log.cmo solver/formula_intf.cmo solver/theory_intf.cmo solver/plugin_intf.cmo solver/expr_intf.cmo solver/tseitin_intf.cmo solver/solver_types_intf.cmo solver/solver_types.cmo solver/res_intf.cmo solver/res.cmo solver/solver_intf.cmo solver/internal.cmo solver/solver.cmo solver/mcsolver.cmo backend/dot.cmo backend/dedukti.cmo solver/tseitin.cmo smt/expr.cmo smt/cnf.cmo sat/sat.cmo smt/sig.cmi smt/unionfind.cmo smt/cc.cmo smt/mcsat.cmo smt/smt.cmo -o msat.cmo - + ocamlfind ocamldep -modules util/hstring.ml > util/hstring.ml.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/hstring.cmo util/hstring.ml - + ocamlfind ocamldep -modules util/hashcons.ml > util/hashcons.ml.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/hashcons.cmo util/hashcons.ml - + ocamlfind ocamldep -modules util/either.ml > util/either.ml.depends - + ocamlfind ocamldep -modules util/vec.ml > util/vec.ml.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/either.cmo util/either.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/vec.cmo util/vec.ml - + ocamlfind ocamldep -modules util/iheap.ml > util/iheap.ml.depends - + ocamlfind ocamldep -modules util/sparse_vec.mli > util/sparse_vec.mli.depends - + ocamlfind ocamlc -c -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/sparse_vec.cmi util/sparse_vec.mli - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/iheap.cmo util/iheap.ml - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/iheap.cmo util/iheap.ml - File "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 util/sparse_vec.ml > util/sparse_vec.ml.depends - + ocamlfind ocamlc -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/sparse_vec.cmo util/sparse_vec.ml - + ocamlfind ocamlc -a -I backend -I util backend/backend_intf.cmo util/either.cmo util/hashcons.cmo util/hstring.cmo util/sparse_vec.cmo util/vec.cmo util/iheap.cmo msat.cmo -o msat.cma - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/hashcons.cmx util/hashcons.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/hstring.cmx util/hstring.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/expr_intf.cmx solver/expr_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/formula_intf.cmx solver/formula_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -for-pack Msat -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/either.cmx util/either.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/vec.cmx util/vec.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver_types_intf.cmx solver/solver_types_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver_types.cmx solver/solver_types.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver_types.cmx solver/solver_types.ml - File "solver/solver_types.ml", line 200, characters 6-14: - 200 | let destruct = Either.destruct - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value destruct. - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 30 -for-pack Msat -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/log.cmx util/log.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/res_intf.cmx solver/res_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/res.cmx solver/res.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/res.cmx solver/res.ml - File "solver/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 "solver/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 "solver/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 -safe-string -short-paths -w K -w X -w Y -strict-sequence -for-pack Msat -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/sparse_vec.cmx util/sparse_vec.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/plugin_intf.cmx solver/plugin_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/iheap.cmx util/iheap.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I util -I backend -I smt -I solver -I sat -I util/smtlib -o util/iheap.cmx util/iheap.ml - File "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 -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/internal.cmx solver/internal.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/internal.cmx solver/internal.ml - File "solver/internal.ml", line 197, characters 57-75: - 197 | module Mi = Map.Make(struct type t = int let compare = Pervasives.compare end) - ^^^^^^^^^^^^^^^^^^ - 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 "solver/internal.ml", line 519, characters 41-59: - 519 | let learnt = List.sort (fun a b -> Pervasives.compare b.var.v_level a.var.v_level) !c in - ^^^^^^^^^^^^^^^^^^ - 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 "solver/internal.ml", line 222, characters 6-14: - 222 | let f_filter i = - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value f_filter. - File "solver/internal.ml", line 278, characters 6-16: - 278 | let nb_learnts () = Vec.size env.clauses_learnt - ^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value nb_learnts. - File "solver/internal.ml", line 855, characters 6-22: - 855 | let remove_satisfied vec = - ^^^^^^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value remove_satisfied. - File "solver/internal.ml", line 954, characters 6-15: - 954 | let check_vec vec = - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value check_vec. - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver_intf.cmx solver/solver_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/theory_intf.cmx solver/theory_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -for-pack Msat -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/backend_intf.cmx backend/backend_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/tseitin_intf.cmx solver/tseitin_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/expr.cmx smt/expr.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/expr.cmx smt/expr.ml - File "smt/expr.ml", line 48, characters 14-32: - 48 | 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 "smt/expr.ml", line 63, characters 16-34: - 63 | 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 "smt/expr.ml", line 71, characters 16-34: - 71 | 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 - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/tseitin.cmx solver/tseitin.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/tseitin.cmx solver/tseitin.ml - File "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 -safe-string -short-paths -w K -w X -w Y -strict-sequence -for-pack Msat -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dot.cmx backend/dot.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -for-pack Msat -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dot.cmx backend/dot.ml - File "backend/dot.ml", line 51, characters 6-11: - 51 | let ttify f c = fun fmt () -> f fmt c - ^^^^^ - Warning 32 [unused-value-declaration]: unused value ttify. - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver.cmx solver/solver.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/solver.cmx solver/solver.ml - File "solver/solver.ml", line 96, characters 6-17: - 96 | let proof_debug _ = assert false - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value proof_debug. - File "solver/solver.ml", line 116, characters 2-25: - 116 | type clause = St.clause - ^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type clause. - File "solver/solver.ml", line 117, characters 2-26: - 117 | type proof = Proof.proof - ^^^^^^^^^^^^^^^^^^^^^^^^ - Warning 34 [unused-type-declaration]: unused type proof. - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/unionfind.cmx smt/unionfind.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 50 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/mcsolver.cmx solver/mcsolver.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/cc.cmx smt/cc.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -for-pack Msat -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dedukti.cmx backend/dedukti.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -for-pack Msat -I backend -I smt -I solver -I util -I sat -I util/smtlib -o backend/dedukti.cmx backend/dedukti.ml - File "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 "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 -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/cnf.cmx smt/cnf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I sat -I backend -I smt -I solver -I util -I util/smtlib -o sat/sat.cmx sat/sat.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I sat -I backend -I smt -I solver -I util -I util/smtlib -o sat/sat.cmx sat/sat.ml - File "sat/sat.ml", line 36, characters 26-44: - 36 | 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 "sat/sat.ml", line 75, characters 12-23: - 75 | let clause_name c = St.(c.name) - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value clause_name. - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/mcsat.cmx smt/mcsat.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/smt.cmx smt/smt.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -I smt -I backend -I solver -I util -I sat -I util/smtlib -o smt/smt.cmx smt/smt.ml - File "smt/smt.ml", line 66, characters 10-21: - 66 | let clause_name c = St.(c.name) - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value clause_name. - + touch msat.mli ; if ocamlfind ocamlopt -pack -g -I util -I solver -I backend -I smt -I sat util/log.cmx solver/formula_intf.cmx solver/theory_intf.cmx solver/plugin_intf.cmx solver/expr_intf.cmx solver/tseitin_intf.cmx solver/solver_types_intf.cmx solver/solver_types.cmx solver/res_intf.cmx solver/res.cmx solver/solver_intf.cmx solver/internal.cmx solver/solver.cmx solver/mcsolver.cmx backend/dot.cmx backend/dedukti.cmx solver/tseitin.cmx smt/expr.cmx smt/cnf.cmx sat/sat.cmx smt/sig.cmi smt/unionfind.cmx smt/cc.cmx smt/mcsat.cmx smt/smt.cmx -o msat.cmx ; then rm -f msat.mli ; else rm -f msat.mli ; exit 1; fi - + ocamlfind ocamlopt -a -I backend -I util backend/backend_intf.cmx util/either.cmx util/hashcons.cmx util/hstring.cmx util/sparse_vec.cmx util/vec.cmx util/iheap.cmx msat.cmx -o msat.cmxa - + ocamlfind ocamlopt -shared -linkall msat.cmxa -o msat.cmxs -> compiled msat.0.3 [msat: make install] + /usr/bin/make "install" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.3) - ocamlbuild -log build.log -use-ocamlfind -classic-display -Is solver,sat,smt,backend,util,util/smtlib msat.cma msat.cmxa msat.cmxs - + ocamlfind ocamlc -config - ocamlfind install msat META _build/msat.cma _build/msat.cmxa _build/msat.cmxs _build/msat.a _build/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.3 === STDERR === 2026-06-16 11:47.05: OK: build msat.0.3 (runc: 9.1s, disk: 41KB) 2026-06-16 11:47.05: Job succeeded