Build:
- 0
2026-06-24 11:05.49: New job: build msat.0.1 (7acd06ce23a2) 2026-06-24 11:05.49: Waiting for resource in pool day11-builds 2026-06-24 11:17.57: Got resource from pool day11-builds 2026-06-24 11:17.57: [profile full] build msat.0.1 2026-06-24 11:17.57: build msat.0.1 (7acd06ce23a2) === DEPENDENCIES (6 transitive) === base-unix.base 7d1428be9ddb 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.1: dl] [msat.0.1: extract] -> retrieved msat.0.1 (https://opam.ocaml.org/cache) [msat: make lib] + /usr/bin/make "lib" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.1) - 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/log_intf.ml > solver/log_intf.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 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/log_intf.cmo solver/log_intf.ml - + ocamlfind ocamldep -modules solver/solver_types_intf.ml > solver/solver_types_intf.ml.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/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/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 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 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/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 util/either.mli > util/either.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 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 169, characters 57-75: - 169 | 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 405, characters 41-59: - 405 | let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.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 194, characters 6-14: - 194 | let f_filter i = - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value f_filter. - File "solver/internal.ml", line 252, characters 6-16: - 252 | let nb_learnts () = Vec.size env.clauses_learnt - ^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value nb_learnts. - File "solver/internal.ml", line 731, characters 6-15: - 731 | let f_sort_db c1 c2 = - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value f_sort_db. - File "solver/internal.ml", line 743, characters 6-12: - 743 | let locked c = false (* - ^^^^^^ - Warning 32 [unused-value-declaration]: unused value locked. - File "solver/internal.ml", line 863, characters 6-15: - 863 | 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 70, characters 8-19: - 70 | let proof_debug _ = assert false - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value proof_debug. - + 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 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 58, characters 26-44: - 58 | 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 - + 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 95, characters 10-21: - 95 | let clause_name c = SatSolver.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 65, characters 10-21: - 65 | let clause_name c = SmtSolver.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/log_intf.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/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/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/vec.cmo util/vec.ml - + ocamlfind ocamldep -modules util/either.ml > util/either.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 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 -package unix -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 -package unix -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 1000 -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 1000 -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 -package unix -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 1000 -for-pack Msat -I solver -I backend -I smt -I util -I sat -I util/smtlib -o solver/log_intf.cmx solver/log_intf.ml - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 100 -for-pack Msat -package unix -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 -for-pack Msat -package unix -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 1000 -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 1000 -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 -for-pack Msat -package unix -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 1000 -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 1000 -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 100 -for-pack Msat -package unix -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 -package unix -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 1000 -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 1000 -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 58, characters 26-44: - 58 | 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 - + ocamlfind ocamlopt -c -g -safe-string -short-paths -w K -w X -w Y -strict-sequence -inline 1000 -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 1000 -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 169, characters 57-75: - 169 | 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 405, characters 41-59: - 405 | let learnt = List.sort (fun a b -> Pervasives.compare b.var.level a.var.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 194, characters 6-14: - 194 | let f_filter i = - ^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value f_filter. - File "solver/internal.ml", line 252, characters 6-16: - 252 | let nb_learnts () = Vec.size env.clauses_learnt - ^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value nb_learnts. - File "solver/internal.ml", line 731, characters 6-15: - 731 | let f_sort_db c1 c2 = - ^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value f_sort_db. - File "solver/internal.ml", line 743, characters 6-12: - 743 | let locked c = false (* - ^^^^^^ - Warning 32 [unused-value-declaration]: unused value locked. - File "solver/internal.ml", line 863, characters 6-15: - 863 | 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 1000 -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 1000 -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 1000 -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 1000 -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 1000 -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 1000 -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 70, characters 8-19: - 70 | let proof_debug _ = assert false - ^^^^^^^^^^^ - Warning 32 [unused-value-declaration]: unused value proof_debug. - + 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 1000 -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 95, characters 10-21: - 95 | let clause_name c = SatSolver.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 65, characters 10-21: - 65 | let clause_name c = SmtSolver.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/log_intf.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/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.1 [msat: make install] + /usr/bin/make "install" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.1) - 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.1 === STDERR === 2026-06-24 11:18.35: OK: build msat.0.1 (runc: 8.6s, disk: 39KB) 2026-06-24 11:18.35: Job succeeded