Build:
- 0
2026-06-24 11:05.49: New job: build msat.0.7 (bce016da7cec) 2026-06-24 11:05.49: Waiting for resource in pool day11-builds 2026-06-24 11:17.44: Got resource from pool day11-builds 2026-06-24 11:17.44: [profile full] build msat.0.7 2026-06-24 11:17.44: build msat.0.7 (bce016da7cec) === 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.7: dl] [msat.0.7: extract] -> retrieved msat.0.7 (https://opam.ocaml.org/cache) [msat: make disable_log] + /usr/bin/make "disable_log" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.7) - 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.7) - 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/backend/dimacs.mli > src/backend/dimacs.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/dimacs.cmi src/backend/dimacs.mli - + 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/coq.mli > src/backend/coq.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/coq.cmi src/backend/coq.mli - + ocamlfind ocamldep -modules src/backend/coq.ml > src/backend/coq.ml.depends - + ocamlfind ocamldep -modules src/backend/dimacs.ml > src/backend/dimacs.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 546, characters 6-18: - 546 | 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 837, characters 12-24: - 837 | 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 901, characters 12-24: - 901 | 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 976, characters 10-22: - 976 | enqueue_bool p lvl (Bcp c) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 1070, characters 8-20: - 1070 | enqueue_bool atom current_level Decision - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - + 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/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/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 29, characters 26-44: - 29 | 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 -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/coq.cmo src/backend/coq.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/dimacs.cmo src/backend/dimacs.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 - + 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/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 - + 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/backend/dimacs.cmo src/core/external.cmo src/solver/solver.cmo src/solver/mcsolver.cmo src/backend/backend_intf.cmo src/backend/dot.cmo src/backend/coq.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 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/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 29, characters 26-44: - 29 | 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 -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/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 546, characters 6-18: - 546 | 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 837, characters 12-24: - 837 | 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 901, characters 12-24: - 901 | 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 976, characters 10-22: - 976 | enqueue_bool p lvl (Bcp c) - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - File "src/core/internal.ml", line 1070, characters 8-20: - 1070 | enqueue_bool atom current_level Decision - ^^^^^^^^^^^^ - Warning 6 [labels-omitted]: label level was omitted in the application of this function. - + 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/backend -I src -I src/mcsat -I src/core -I src/smt -I src/solver -I src/util -I src/sat -o src/backend/dimacs.cmx src/backend/dimacs.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/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/coq.cmx src/backend/coq.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 - + 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/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 - + 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/backend/dimacs.cmx src/core/external.cmx src/solver/solver.cmx src/solver/mcsolver.cmx src/backend/backend_intf.cmx src/backend/dot.cmx src/backend/coq.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.7 [msat: make install] + /usr/bin/make "DOCDIR=/home/opam/.opam/default/doc/msat" "install" (CWD=/home/opam/.opam/default/.opam-switch/build/msat.0.7) - 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.7 === STDERR === 2026-06-24 11:18.17: OK: build msat.0.7 (runc: 7.6s, disk: 35KB) 2026-06-24 11:18.17: Job succeeded