Build:
- 0
2026-06-16 13:48.20: New job: build alt-ergo-lib.2.4.2 (ed496d7ee11e)
2026-06-16 13:48.20: Waiting for resource in pool day11-builds
2026-06-16 15:19.07: Got resource from pool day11-builds
2026-06-16 15:19.07: [profile full] build alt-ergo-lib.2.4.2
2026-06-16 15:19.07: build alt-ergo-lib.2.4.2 (ed496d7ee11e)
=== DEPENDENCIES (18 transitive) ===
base-threads.base b7164ff76afe
base-unix.base 839dc585f12d
conf-autoconf.0.2 b3cd190cf0b5
conf-gmp.5 61e3c79e0ddf
conf-pkg-config.5 64c6b37d622b
csexp.1.5.2 e2491a88a8e9
dune.3.23.1 d50060dd2cab
dune-configurator.3.23.1 83dd42d9abe2
num.1.6 158dee1e5f8c
ocaml.5.4.1 708fed352b2a
ocaml-base-compiler.5.4.1 89b85703f841
ocaml-compiler.5.4.1 a719b8419b8e
ocaml-config.3 aa27f63940d8
ocamlfind.1.9.8 5cfa73ef65e7
ocplib-simplex.0.4.1 c637333be0d1
seq.base 75c7a6b170f3
stdlib-shims.0.3.0 b64bd5274094
zarith.1.14 b2ef7cdb0e39
=== STDOUT ===
Processing: [default: loading data]
[alt-ergo-lib.2.4.2: dl]
[alt-ergo-lib.2.4.2: extract]
[alt-ergo-lib.2.4.2/version_update.patch: dl]
-> retrieved alt-ergo-lib.2.4.2 (https://opam.ocaml.org/cache)
[alt-ergo-lib: patch] applying version_update.patch
[alt-ergo-lib: ocaml unix.cma]
+ /home/opam/.opam/default/bin/ocaml "unix.cma" "configure.ml" "alt-ergo-lib" "--prefix" "/home/opam/.opam/default" "--libdir" "/home/opam/.opam/default/lib" "--mandir" "/home/opam/.opam/default/man" (CWD=/home/opam/.opam/default/.opam-switch/build/alt-ergo-lib.2.4.2)
- File "_none_", line 1:
- Alert ocaml_deprecated_auto_include:
- OCaml's lib directory layout changed in 5.0. The unix subdirectory has been
- automatically added to the search path, but you should add -I +unix to the
- command-line to silence this alert (e.g. by adding unix to the list of
- libraries in your dune file, or adding use_unix to your _tags file for
- ocamlbuild, or using -package unix for ocamlfind).
-
- File "_none_", line 1:
- Alert ocaml_deprecated_auto_include:
- OCaml's lib directory layout changed in 5.0. The unix subdirectory has been
- automatically added to the search path, but you should add -I +unix to the
- command-line to silence this alert (e.g. by adding unix to the list of
- libraries in your dune file, or adding use_unix to your _tags file for
- ocamlbuild, or using -package unix for ocamlfind).
- Using provided value for 'prefix' : /home/opam/.opam/default
- Using provided value for 'libdir' : /home/opam/.opam/default/lib
- Using provided value for 'mandir' : /home/opam/.opam/default/man
- Generating file src/lib/util/config.ml...done.
- Generating file src/bin/text/flags.dune...done.
- Generating file Makefile.config...done.
- Good to go!
[alt-ergo-lib: dune build]
+ /home/opam/.opam/default/bin/dune "build" "-p" "alt-ergo-lib" "-j" "39" (CWD=/home/opam/.opam/default/.opam-switch/build/alt-ergo-lib.2.4.2)
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Util.cmi -c -intf src/lib/util/util.mli)
- File "src/lib/util/util.mli", line 63, characters 6-12:
- 63 | val [@inline always] compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int
- ^^^^^^
- Warning 53 [misplaced-attribute]: the inline attribute cannot appear in this context
-
- File "src/lib/util/util.mli", line 65, characters 6-12:
- 65 | val [@inline always] cmp_lists: 'a list -> 'a list -> ('a -> 'a -> int) -> int
- ^^^^^^
- Warning 53 [misplaced-attribute]: the inline attribute cannot appear in this context
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Parsed_interface.cmi -c -intf src/lib/frontend/parsed_interface.mli)
- File "src/lib/frontend/parsed_interface.mli", line 18, characters 20-77:
- 18 | [@ocaml.ppwarning "TODO: add documentation for every function in this file"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add documentation for every function in this file
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Ty.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Ty.cmo -c -impl src/lib/structures/ty.ml)
- File "src/lib/structures/ty.ml", line 200, characters 20-51:
- 200 | [@ocaml.ppwarning "TODO: should be implemented ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should be implemented ?
-
- File "src/lib/structures/ty.ml", line 334, characters 24-65:
- 334 | [@ocaml.ppwarning "TODO: detect when there are no changes "]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: detect when there are no changes
-
- File "src/lib/structures/ty.ml", line 589, characters 28-59:
- 589 | | _ , _ [@ocaml.ppwarning "TODO: remove fragile pattern "] ->
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: remove fragile pattern
-
- File "src/lib/structures/ty.ml", line 639, characters 20-61:
- 639 | [@ocaml.ppwarning "TODO: detect when there are no changes "]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: detect when there are no changes
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Records.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Records.cmo -c -impl src/lib/reasoners/records.ml)
- File "src/lib/reasoners/records.ml", line 283, characters 26-69:
- 283 | [@ocaml.ppwarning "TODO: should not rebuild if not changed !"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should not rebuild if not changed !
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Adt.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Adt.cmo -c -impl src/lib/reasoners/adt.ml)
- File "src/lib/reasoners/adt.ml", lines 63-64, characters 21-30:
- 63 | ....................."XXX: IsConstr not interpreted currently. Maybe \
- 64 | it's OK".
- Warning 22 [preprocessor]: XXX: IsConstr not interpreted currently. Maybe it's OK
-
- File "src/lib/reasoners/adt.ml", line 105, characters 24-64:
- 105 | [@ocaml.ppwarning "TODO: canonize Constr(list of selects)"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: canonize Constr(list of selects)
-
- File "src/lib/reasoners/adt.ml", line 227, characters 21-37:
- 227 | [@@ocaml.ppwarning "TODO: not sure"]
- ^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: not sure
-
- File "src/lib/reasoners/adt.ml", line 318, characters 24-50:
- 318 | [@ocaml.ppwarning "TODO: abstract Selectors"] ->
- ^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: abstract Selectors
-
- File "src/lib/reasoners/adt.ml", line 305, characters 26-66:
- 305 | [@ocaml.ppwarning "TODO: abstract Selectors: case to test"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: abstract Selectors: case to test
-
- File "src/lib/reasoners/adt.ml", line 313, characters 27-67:
- 313 | [@ocaml.ppwarning "TODO: abstract Selectors: case to test"] then
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: abstract Selectors: case to test
-
- File "src/lib/reasoners/adt.ml", line 328, characters 27-53:
- 328 | [@ocaml.ppwarning "TODO: abstract Selectors"] then
- ^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: abstract Selectors
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml_types.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml_types.cmo -c -impl src/lib/structures/satml_types.ml)
- File "src/lib/structures/satml_types.ml", line 852, characters 33-71:
- 852 | [@ocaml.ppwarning "xlit or at_lit is probably redundant"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: xlit or at_lit is probably redundant
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Cnf.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Cnf.cmo -c -impl src/lib/frontend/cnf.ml)
- File "src/lib/frontend/cnf.ml", lines 38-40, characters 19-33:
- 38 | ..................."TODO: Change Symbols.Float to store FP numeral \
- 39 | constants (eg, <24, -149> for single) instead of \
- 40 | having terms".
- Warning 22 [preprocessor]: TODO: Change Symbols.Float to store FP numeral constants (eg, <24, -149> for single) instead of having terms
-
- File "src/lib/frontend/cnf.ml", line 250, characters 29-64:
- 250 | [@ocaml.ppwarning "TODO: should introduce fresh vars"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should introduce fresh vars
-
- File "src/lib/frontend/cnf.ml", line 475, characters 29-64:
- 475 | [@ocaml.ppwarning "TODO: should introduce fresh vars"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should introduce fresh vars
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Ite_rel.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Ite_rel.cmo -c -impl src/lib/reasoners/ite_rel.ml)
- File "src/lib/reasoners/ite_rel.ml", line 119, characters 35-62:
- 119 | [@ocaml.ppwarning "TODO: build IFF instead ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: build IFF instead ?
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Adt_rel.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Adt_rel.cmo -c -impl src/lib/reasoners/adt_rel.ml)
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 296-297, characters 19-66:
- 296 | ..................."XXX improve. For each selector, store its \
- 297 | corresponding constructor when typechecking ?".
- Warning 22 [preprocessor]: XXX improve. For each selector, store its corresponding constructor when typechecking ?
-
- File "src/lib/reasoners/adt_rel.ml", line 334, characters 19-72:
- 334 | [@@ocaml.ppwarning "working with X.term_extract r would be sufficient ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: working with X.term_extract r would be sufficient ?
-
- File "src/lib/reasoners/adt_rel.ml", line 648, characters 31-77:
- 648 | [@ocaml.ppwarning "XXX: assume not (. ? .): reasoning missing ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: XXX: assume not (. ? .): reasoning missing ?
-
- File "src/lib/reasoners/adt_rel.ml", line 709, characters 26-72:
- 709 | [@ocaml.ppwarning "XXX: assume not (. ? .): reasoning missing ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: XXX: assume not (. ? .): reasoning missing ?
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Ty.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Ty.cmx -c -impl src/lib/structures/ty.ml)
- File "src/lib/structures/ty.ml", line 200, characters 20-51:
- 200 | [@ocaml.ppwarning "TODO: should be implemented ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should be implemented ?
-
- File "src/lib/structures/ty.ml", line 334, characters 24-65:
- 334 | [@ocaml.ppwarning "TODO: detect when there are no changes "]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: detect when there are no changes
-
- File "src/lib/structures/ty.ml", line 589, characters 28-59:
- 589 | | _ , _ [@ocaml.ppwarning "TODO: remove fragile pattern "] ->
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: remove fragile pattern
-
- File "src/lib/structures/ty.ml", line 639, characters 20-61:
- 639 | [@ocaml.ppwarning "TODO: detect when there are no changes "]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: detect when there are no changes
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Shostak.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Shostak.cmo -c -impl src/lib/reasoners/shostak.ml)
- File "src/lib/reasoners/shostak.ml", lines 551-553, characters 26-39:
- 551 | .........................."TODO: a simple way of handling equalities \
- 552 | with void and unit is to add this case is \
- 553 | the solver!".
- Warning 22 [preprocessor]: TODO: a simple way of handling equalities with void and unit is to add this case is the solver!
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml_frontend.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml_frontend.cmo -c -impl src/lib/reasoners/satml_frontend.ml)
- File "src/lib/reasoners/satml_frontend.ml", line 374, characters 24-77:
- 374 | [@ocaml.ppwarning "TODO: modifications made in tbox are lost! improve?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: modifications made in tbox are lost! improve?
-
- File "src/lib/reasoners/satml_frontend.ml", lines 671-672, characters 6-63:
- 671 | ......"improve terms / atoms extraction in lazy/non-lazy \
- 672 | and greedy/non-greedy mode. Separate atoms from terms !".
- Warning 22 [preprocessor]: improve terms / atoms extraction in lazy/non-lazy and greedy/non-greedy mode. Separate atoms from terms !
-
- File "src/lib/reasoners/satml_frontend.ml", line 693, characters 22-75:
- 693 | [@ocaml.ppwarning "Issue for greedy: terms inside lemmas not extracted"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: Issue for greedy: terms inside lemmas not extracted
-
- File "src/lib/reasoners/satml_frontend.ml", lines 714-715, characters 22-73:
- 714 | ......................"!!! Possibles issues du to replacement of atoms \
- 715 | that are facts with TRUE by mk_lit (and simplify)".
- Warning 22 [preprocessor]: !!! Possibles issues du to replacement of atoms that are facts with TRUE by mk_lit (and simplify)
-
- File "src/lib/reasoners/satml_frontend.ml", line 748, characters 28-61:
- 748 | [@ocaml.ppwarning "TODO: should be assert failure?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should be assert failure?
-
- File "src/lib/reasoners/satml_frontend.ml", line 846, characters 34-79:
- 846 | [@ocaml.ppwarning "TODO: should fix for unsat cores generation"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should fix for unsat cores generation
-
- File "src/lib/reasoners/satml_frontend.ml", line 985, characters 20-79:
- 985 | "TODO: first intantiation a la DfsSAT before searching ..."]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: first intantiation a la DfsSAT before searching ...
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml.cmo -c -impl src/lib/reasoners/satml.ml)
- File "src/lib/reasoners/satml.ml", line 523, characters 26-66:
- 523 | [@ocaml.ppwarning "TODO: try to disable 'fill_with_dummy'"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: try to disable 'fill_with_dummy'
-
- File "src/lib/reasoners/satml.ml", lines 1576-1579, characters 28-42:
- 1576 | ............................"TODO: add a heavy assert that checks \
- 1577 | that clauses are not redundant, watchs \
- 1578 | are well set, unit and bottom are \
- 1579 | detected ...".
- Warning 22 [preprocessor]: TODO: add a heavy assert that checks that clauses are not redundant, watchs are well set, unit and bottom are detected ...
-
- File "src/lib/reasoners/satml.ml", lines 1645-1646, characters 22-43:
- 1645 | ......................"Issue: BAD decision_level, in particular, \
- 1646 | if minimal-bj is ON".
- Warning 22 [preprocessor]: Issue: BAD decision_level, in particular, if minimal-bj is ON
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__IntervalCalculus.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__IntervalCalculus.cmo -c -impl src/lib/reasoners/intervalCalculus.ml)
- File "src/lib/reasoners/intervalCalculus.ml", line 1838, characters 27-63:
- 1838 | [@ocaml.ppwarning "TODO: add other terms such as div!"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add other terms such as div!
-
- File "src/lib/reasoners/intervalCalculus.ml", line 2091, characters 28-73:
- 2091 | [@ocaml.ppwarning "TODO: find an example triggering this case!"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: find an example triggering this case!
- (cd _build/default && /home/opam/.opam/default/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -bin-annot-occurrences -I src/lib/.AltErgoLib.objs/byte -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Expr.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Expr.cmo -c -impl src/lib/structures/expr.ml)
- File "src/lib/structures/expr.ml", line 1387, characters 33-66:
- 1387 | else acc [@ocaml.ppwarning "TODO: add some stuff from let_e"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add some stuff from let_e
-
- File "src/lib/structures/expr.ml", lines 1599-1601, characters 24-55:
- 1599 | ........................"TODO: should also inline form in form. But \
- 1600 | not possible to detect if we are not \
- 1601 | inlining a form inside a term".
- Warning 22 [preprocessor]: TODO: should also inline form in form. But not possible to detect if we are not inlining a form inside a term
-
- File "src/lib/structures/expr.ml", lines 2094-2097, characters 34-77:
- 2094 | .................................."TODO: once 'let x = term in term' \
- 2095 | added, check that the resulting sbt \
- 2096 | is well normalized (may be not true \
- 2097 | depending on the ordering of vars in lets".
- Warning 22 [preprocessor]: TODO: once 'let x = term in term' added, check that the resulting sbt is well normalized (may be not true depending on the ordering of vars in lets
-
- File "src/lib/structures/expr.ml", lines 2118-2120, characters 26-49:
- 2118 | .........................."TODO: do it for this case once \
- 2119 | free-vars issues of theories axioms \
- 2120 | with hypotheses fixed".
- Warning 22 [preprocessor]: TODO: do it for this case once free-vars issues of theories axioms with hypotheses fixed
-
- File "src/lib/structures/expr.ml", lines 2114-2116, characters 26-56:
- 2114 | .........................."TODO: filter_good_triggers for this \
- 2115 | case once free-vars issues of theories \
- 2116 | axioms with hypotheses fixed".
- Warning 22 [preprocessor]: TODO: filter_good_triggers for this case once free-vars issues of theories axioms with hypotheses fixed
-
- File "src/lib/structures/expr.ml", line 2320, characters 20-57:
- 2320 | [@ocaml.ppwarning "TODO: add a match construct in expr"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add a match construct in expr
-
- File "src/lib/structures/expr.ml", line 2319, characters 20-50:
- 2319 | [@ocaml.ppwarning "TODO: add other elim schemes"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add other elim schemes
-
- File "src/lib/structures/expr.ml", line 2318, characters 20-62:
- 2318 | [@ocaml.ppwarning "TODO: introduce a let if e is a big expr"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: introduce a let if e is a big expr
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Expr.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Expr.cmx -c -impl src/lib/structures/expr.ml)
- File "src/lib/structures/expr.ml", line 1387, characters 33-66:
- 1387 | else acc [@ocaml.ppwarning "TODO: add some stuff from let_e"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add some stuff from let_e
-
- File "src/lib/structures/expr.ml", lines 1599-1601, characters 24-55:
- 1599 | ........................"TODO: should also inline form in form. But \
- 1600 | not possible to detect if we are not \
- 1601 | inlining a form inside a term".
- Warning 22 [preprocessor]: TODO: should also inline form in form. But not possible to detect if we are not inlining a form inside a term
-
- File "src/lib/structures/expr.ml", lines 2094-2097, characters 34-77:
- 2094 | .................................."TODO: once 'let x = term in term' \
- 2095 | added, check that the resulting sbt \
- 2096 | is well normalized (may be not true \
- 2097 | depending on the ordering of vars in lets".
- Warning 22 [preprocessor]: TODO: once 'let x = term in term' added, check that the resulting sbt is well normalized (may be not true depending on the ordering of vars in lets
-
- File "src/lib/structures/expr.ml", lines 2118-2120, characters 26-49:
- 2118 | .........................."TODO: do it for this case once \
- 2119 | free-vars issues of theories axioms \
- 2120 | with hypotheses fixed".
- Warning 22 [preprocessor]: TODO: do it for this case once free-vars issues of theories axioms with hypotheses fixed
-
- File "src/lib/structures/expr.ml", lines 2114-2116, characters 26-56:
- 2114 | .........................."TODO: filter_good_triggers for this \
- 2115 | case once free-vars issues of theories \
- 2116 | axioms with hypotheses fixed".
- Warning 22 [preprocessor]: TODO: filter_good_triggers for this case once free-vars issues of theories axioms with hypotheses fixed
-
- File "src/lib/structures/expr.ml", line 2320, characters 20-57:
- 2320 | [@ocaml.ppwarning "TODO: add a match construct in expr"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add a match construct in expr
-
- File "src/lib/structures/expr.ml", line 2319, characters 20-50:
- 2319 | [@ocaml.ppwarning "TODO: add other elim schemes"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add other elim schemes
-
- File "src/lib/structures/expr.ml", line 2318, characters 20-62:
- 2318 | [@ocaml.ppwarning "TODO: introduce a let if e is a big expr"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: introduce a let if e is a big expr
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Records.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Records.cmx -c -impl src/lib/reasoners/records.ml)
- File "src/lib/reasoners/records.ml", line 283, characters 26-69:
- 283 | [@ocaml.ppwarning "TODO: should not rebuild if not changed !"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should not rebuild if not changed !
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Adt.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Adt.cmx -c -impl src/lib/reasoners/adt.ml)
- File "src/lib/reasoners/adt.ml", lines 63-64, characters 21-30:
- 63 | ....................."XXX: IsConstr not interpreted currently. Maybe \
- 64 | it's OK".
- Warning 22 [preprocessor]: XXX: IsConstr not interpreted currently. Maybe it's OK
-
- File "src/lib/reasoners/adt.ml", line 105, characters 24-64:
- 105 | [@ocaml.ppwarning "TODO: canonize Constr(list of selects)"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: canonize Constr(list of selects)
-
- File "src/lib/reasoners/adt.ml", line 227, characters 21-37:
- 227 | [@@ocaml.ppwarning "TODO: not sure"]
- ^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: not sure
-
- File "src/lib/reasoners/adt.ml", line 318, characters 24-50:
- 318 | [@ocaml.ppwarning "TODO: abstract Selectors"] ->
- ^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: abstract Selectors
-
- File "src/lib/reasoners/adt.ml", line 305, characters 26-66:
- 305 | [@ocaml.ppwarning "TODO: abstract Selectors: case to test"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: abstract Selectors: case to test
-
- File "src/lib/reasoners/adt.ml", line 313, characters 27-67:
- 313 | [@ocaml.ppwarning "TODO: abstract Selectors: case to test"] then
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: abstract Selectors: case to test
-
- File "src/lib/reasoners/adt.ml", line 328, characters 27-53:
- 328 | [@ocaml.ppwarning "TODO: abstract Selectors"] then
- ^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: abstract Selectors
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Cnf.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Cnf.cmx -c -impl src/lib/frontend/cnf.ml)
- File "src/lib/frontend/cnf.ml", lines 38-40, characters 19-33:
- 38 | ..................."TODO: Change Symbols.Float to store FP numeral \
- 39 | constants (eg, <24, -149> for single) instead of \
- 40 | having terms".
- Warning 22 [preprocessor]: TODO: Change Symbols.Float to store FP numeral constants (eg, <24, -149> for single) instead of having terms
-
- File "src/lib/frontend/cnf.ml", line 250, characters 29-64:
- 250 | [@ocaml.ppwarning "TODO: should introduce fresh vars"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should introduce fresh vars
-
- File "src/lib/frontend/cnf.ml", line 475, characters 29-64:
- 475 | [@ocaml.ppwarning "TODO: should introduce fresh vars"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should introduce fresh vars
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml_types.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Satml_types.cmx -c -impl src/lib/structures/satml_types.ml)
- File "src/lib/structures/satml_types.ml", line 852, characters 33-71:
- 852 | [@ocaml.ppwarning "xlit or at_lit is probably redundant"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: xlit or at_lit is probably redundant
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Shostak.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Shostak.cmx -c -impl src/lib/reasoners/shostak.ml)
- File "src/lib/reasoners/shostak.ml", lines 551-553, characters 26-39:
- 551 | .........................."TODO: a simple way of handling equalities \
- 552 | with void and unit is to add this case is \
- 553 | the solver!".
- Warning 22 [preprocessor]: TODO: a simple way of handling equalities with void and unit is to add this case is the solver!
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Ite_rel.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Ite_rel.cmx -c -impl src/lib/reasoners/ite_rel.ml)
- File "src/lib/reasoners/ite_rel.ml", line 119, characters 35-62:
- 119 | [@ocaml.ppwarning "TODO: build IFF instead ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: build IFF instead ?
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Adt_rel.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Adt_rel.cmx -c -impl src/lib/reasoners/adt_rel.ml)
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
-
- File "src/lib/reasoners/adt_rel.ml", lines 296-297, characters 19-66:
- 296 | ..................."XXX improve. For each selector, store its \
- 297 | corresponding constructor when typechecking ?".
- Warning 22 [preprocessor]: XXX improve. For each selector, store its corresponding constructor when typechecking ?
-
- File "src/lib/reasoners/adt_rel.ml", line 334, characters 19-72:
- 334 | [@@ocaml.ppwarning "working with X.term_extract r would be sufficient ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: working with X.term_extract r would be sufficient ?
-
- File "src/lib/reasoners/adt_rel.ml", line 648, characters 31-77:
- 648 | [@ocaml.ppwarning "XXX: assume not (. ? .): reasoning missing ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: XXX: assume not (. ? .): reasoning missing ?
-
- File "src/lib/reasoners/adt_rel.ml", line 709, characters 26-72:
- 709 | [@ocaml.ppwarning "XXX: assume not (. ? .): reasoning missing ?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: XXX: assume not (. ? .): reasoning missing ?
-
- File "src/lib/reasoners/adt_rel.ml", lines 41-42, characters 22-51:
- 41 | ......................"selectors should be improved. only representatives \
- 42 | in it. No true or false _is".
- Warning 22 [preprocessor]: selectors should be improved. only representatives in it. No true or false _is
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__IntervalCalculus.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__IntervalCalculus.cmx -c -impl src/lib/reasoners/intervalCalculus.ml)
- File "src/lib/reasoners/intervalCalculus.ml", line 1838, characters 27-63:
- 1838 | [@ocaml.ppwarning "TODO: add other terms such as div!"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: add other terms such as div!
-
- File "src/lib/reasoners/intervalCalculus.ml", line 2091, characters 28-73:
- 2091 | [@ocaml.ppwarning "TODO: find an example triggering this case!"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: find an example triggering this case!
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Satml.cmx -c -impl src/lib/reasoners/satml.ml)
- File "src/lib/reasoners/satml.ml", line 523, characters 26-66:
- 523 | [@ocaml.ppwarning "TODO: try to disable 'fill_with_dummy'"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: try to disable 'fill_with_dummy'
-
- File "src/lib/reasoners/satml.ml", lines 1576-1579, characters 28-42:
- 1576 | ............................"TODO: add a heavy assert that checks \
- 1577 | that clauses are not redundant, watchs \
- 1578 | are well set, unit and bottom are \
- 1579 | detected ...".
- Warning 22 [preprocessor]: TODO: add a heavy assert that checks that clauses are not redundant, watchs are well set, unit and bottom are detected ...
-
- File "src/lib/reasoners/satml.ml", lines 1645-1646, characters 22-43:
- 1645 | ......................"Issue: BAD decision_level, in particular, \
- 1646 | if minimal-bj is ON".
- Warning 22 [preprocessor]: Issue: BAD decision_level, in particular, if minimal-bj is ON
- (cd _build/default && /home/opam/.opam/default/bin/ocamlopt.opt -w -40 -bin-annot -O3 -unbox-closures -I src/lib/.AltErgoLib.objs/byte -I src/lib/.AltErgoLib.objs/native -I /home/opam/.opam/default/lib/num -I /home/opam/.opam/default/lib/ocaml/dynlink -I /home/opam/.opam/default/lib/ocaml/str -I /home/opam/.opam/default/lib/ocaml/unix -I /home/opam/.opam/default/lib/ocplib-simplex -I /home/opam/.opam/default/lib/seq -I /home/opam/.opam/default/lib/stdlib-shims -I /home/opam/.opam/default/lib/zarith -cmi-file src/lib/.AltErgoLib.objs/byte/altErgoLib__Satml_frontend.cmi -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/native/altErgoLib__Satml_frontend.cmx -c -impl src/lib/reasoners/satml_frontend.ml)
- File "src/lib/reasoners/satml_frontend.ml", line 374, characters 24-77:
- 374 | [@ocaml.ppwarning "TODO: modifications made in tbox are lost! improve?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: modifications made in tbox are lost! improve?
-
- File "src/lib/reasoners/satml_frontend.ml", lines 671-672, characters 6-63:
- 671 | ......"improve terms / atoms extraction in lazy/non-lazy \
- 672 | and greedy/non-greedy mode. Separate atoms from terms !".
- Warning 22 [preprocessor]: improve terms / atoms extraction in lazy/non-lazy and greedy/non-greedy mode. Separate atoms from terms !
-
- File "src/lib/reasoners/satml_frontend.ml", line 693, characters 22-75:
- 693 | [@ocaml.ppwarning "Issue for greedy: terms inside lemmas not extracted"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: Issue for greedy: terms inside lemmas not extracted
-
- File "src/lib/reasoners/satml_frontend.ml", lines 714-715, characters 22-73:
- 714 | ......................"!!! Possibles issues du to replacement of atoms \
- 715 | that are facts with TRUE by mk_lit (and simplify)".
- Warning 22 [preprocessor]: !!! Possibles issues du to replacement of atoms that are facts with TRUE by mk_lit (and simplify)
-
- File "src/lib/reasoners/satml_frontend.ml", line 748, characters 28-61:
- 748 | [@ocaml.ppwarning "TODO: should be assert failure?"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should be assert failure?
-
- File "src/lib/reasoners/satml_frontend.ml", line 846, characters 34-79:
- 846 | [@ocaml.ppwarning "TODO: should fix for unsat cores generation"]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: should fix for unsat cores generation
-
- File "src/lib/reasoners/satml_frontend.ml", line 985, characters 20-79:
- 985 | "TODO: first intantiation a la DfsSAT before searching ..."]
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- Warning 22 [preprocessor]: TODO: first intantiation a la DfsSAT before searching ...
-> compiled alt-ergo-lib.2.4.2
-> installed alt-ergo-lib.2.4.2
[WARNING] Opam packages conf-gmp.5 and conf-pkg-config.5 depend on the following system packages that are no longer installed: libgmp-dev pkg-config
- conf-gmp.5: depends on libgmp-dev
- conf-pkg-config.5: depends on pkg-config
=== STDERR ===
2026-06-16 15:23.18: OK: build alt-ergo-lib.2.4.2 (runc: 23.1s, disk: 58KB)
2026-06-16 15:23.18: Job succeeded