Build:
- 0
2024-01-29 15:19.05: New job: Voodoo prep z3_tptp.4.8.13; 15dc5bf36fc07dfa3057fae176151995 2024-01-29 15:19.05: Waiting for resource in pool OCluster 2024-01-29 19:16.16: Waiting for worker… 2024-01-29 19:16.34: Got resource from pool OCluster 2024-01-29 19:16.34: Using cache hint "docs-universe-prep-4.14.1" To reproduce locally: cat > prep.spec <<'END-OF-SPEC' ((build tools ((from ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef) (user (uid 1000) (gid 1000)) (workdir /home/opam) (run (shell "sudo chown opam:opam /home/opam")) (run (network host) (shell "sudo apt-get update && sudo apt-get install -yy m4 pkg-config")) (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "opam pin -ny https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 && opam depext -iy voodoo-prep")) (run (shell "cp $(opam config var bin)/voodoo-prep /home/opam")))) (from ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef) (user (uid 1000) (gid 1000)) (workdir /home/opam) (run (shell "sudo chown opam:opam /home/opam")) (run (shell "sudo mkdir /src")) (copy (src packages) (dst /src/packages)) (copy (src repo) (dst /src/repo)) (run (network host) (shell "sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam && opam init --reinit -ni")) (run (shell "opam repo remove default && opam repo add opam /src")) (copy (from (build tools)) (src /home/opam/voodoo-prep) (dst /home/opam/)) (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "opam install ocamlfind.1.9.6")) (env DUNE_CACHE disabled) (env DUNE_CACHE_TRANSPORT direct) (env DUNE_CACHE_DUPLICATION copy) (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "(sudo apt update) && ((opam depext -viy z3_tptp.4.8.13 zarith.1.13 z3.4.8.13 ocamlfind.1.9.6 conf-python-3.9.0.0 conf-gmp.4 conf-g++.1.0 conf-c++.1.0 2>&1 | tee ~/opam.err.log) || echo 'Failed to install all packages')")) (run (shell "opam exec -- ~/voodoo-prep -u z3_tptp:15dc5bf36fc07dfa3057fae176151995,z3:a5ca7c6c94219d0fa101939a04164a9e")) (run (network host) (secrets (ssh_privkey (target /home/opam/.ssh/id_rsa)) (ssh_pubkey (target /home/opam/.ssh/id_rsa.pub)) (ssh_config (target /home/opam/.ssh/config))) (shell "(echo '0.501061') && (for DATA in prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13,z3.4.8.13-a5ca7c6c94219d0fa101939a04164a9e,z3.4.8.13 prep/universes/15dc5bf36fc07dfa3057fae176151995/z3_tptp/4.8.13,z3_tptp.4.8.13-15dc5bf36fc07dfa3057fae176151995,z3_tptp.4.8.13; do IFS=\",\"; set -- $DATA; ([ -d $1 ] || (echo \"FAILED:$2\" && mkdir -p $1 && cp ~/opam.err.log $1 && opam show $3 --raw > $1/opam)) && (shopt -s nullglob && ((tar -cvf $1.tar $1/* && rm -R $1/* && mv $1.tar $1/content.tar) || (echo 'Empty directory'))) done) && (for DATA in prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13,z3.4.8.13-a5ca7c6c94219d0fa101939a04164a9e,z3.4.8.13 prep/universes/15dc5bf36fc07dfa3057fae176151995/z3_tptp/4.8.13,z3_tptp.4.8.13-15dc5bf36fc07dfa3057fae176151995,z3_tptp.4.8.13; do IFS=\",\"; set -- $DATA; rsync -aR --no-p ./$1 docs.ci.ocaml.org:/data/.; done) && (for DATA in prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13,z3.4.8.13-a5ca7c6c94219d0fa101939a04164a9e,z3.4.8.13 prep/universes/15dc5bf36fc07dfa3057fae176151995/z3_tptp/4.8.13,z3_tptp.4.8.13-15dc5bf36fc07dfa3057fae176151995,z3_tptp.4.8.13; do IFS=\",\"; set -- $DATA; HASH=$((sha256sum $1/content.tar | cut -d \" \" -f 1) || echo -n 'empty'); printf \"HASHES:$2:$HASH\\n\"; done)")) ) END-OF-SPEC ocluster-client submit-obuilder https://github.com/ocaml/opam-repository.git 6c6b9002fe4d4d8cc8a33112090bee94b8c89b36 --local-file prep.spec \ --pool linux-x86_64 --connect ocluster-submission.cap --cache-hint docs-universe-prep-4.14.1 \ --secret ssh_privkey:id_rsa --secret ssh_pubkey:id_rsa.pub--secret ssh_config:ssh_config 2024-01-29 19:16.34: RETRYING: 2024-01-29/151905-voodoo-prep-455cb2 Number of retries: 0 (retriable error condition) Building on asteria.caelum.ci.dev All commits already cached Updating files: 93% (30535/32504) Updating files: 94% (30554/32504) Updating files: 95% (30879/32504) Updating files: 96% (31204/32504) Updating files: 97% (31529/32504) Updating files: 98% (31854/32504) Updating files: 99% (32179/32504) Updating files: 100% (32504/32504) Updating files: 100% (32504/32504), done. HEAD is now at 6c6b9002fe conf-gmp: Add support for distributions derived from fedora (build "tools" …) (from ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef) Unable to find image 'ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef' locally docker.io/ocaml/opam@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef: Pulling from ocaml/opam 82e8c0c7d92b: Pulling fs layer 82e8c0c7d92b: Verifying Checksum 82e8c0c7d92b: Download complete 82e8c0c7d92b: Pull complete Digest: sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef Status: Downloaded newer image for ocaml/opam@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef 2024-01-29 19:11.44 ---> using "1f16aa8fbc1a229ca02cdf7d8b4234eb4608a9074cec5292a9e72517b48fb577" from cache /: (user (uid 1000) (gid 1000)) /: (workdir /home/opam) /home/opam: (run (shell "sudo chown opam:opam /home/opam")) 2024-01-29 19:11.44 ---> using "258ae3900365106d3b475f7327e1977f1a9ae54d4b6cd6e024f1ed5ef4f3381c" from cache /home/opam: (run (network host) (shell "sudo apt-get update && sudo apt-get install -yy m4 pkg-config")) Hit:1 http://deb.debian.org/debian bookworm InRelease Get:2 http://deb.debian.org/debian bookworm-updates InRelease [52.1 kB] Get:3 http://deb.debian.org/debian-security bookworm-security InRelease [48.0 kB] Get:4 http://deb.debian.org/debian-security bookworm-security/main amd64 Packages [134 kB] Fetched 234 kB in 0s (655 kB/s) Reading package lists... Reading package lists... Building dependency tree... Reading state information... The following additional packages will be installed: libpkgconf3 pkgconf pkgconf-bin Suggested packages: m4-doc The following NEW packages will be installed: libpkgconf3 m4 pkg-config pkgconf pkgconf-bin 0 upgraded, 5 newly installed, 0 to remove and 0 not upgraded. Need to get 392 kB of archives. After this operation, 969 kB of additional disk space will be used. Get:1 http://deb.debian.org/debian bookworm/main amd64 libpkgconf3 amd64 1.8.1-1 [36.1 kB] Get:2 http://deb.debian.org/debian bookworm/main amd64 m4 amd64 1.4.19-3 [287 kB] Get:3 http://deb.debian.org/debian bookworm/main amd64 pkgconf-bin amd64 1.8.1-1 [29.5 kB] Get:4 http://deb.debian.org/debian bookworm/main amd64 pkgconf amd64 1.8.1-1 [25.9 kB] Get:5 http://deb.debian.org/debian bookworm/main amd64 pkg-config amd64 1.8.1-1 [13.7 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 392 kB in 0s (1497 kB/s) Selecting previously unselected package libpkgconf3:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 18743 files and directories currently installed.) Preparing to unpack .../libpkgconf3_1.8.1-1_amd64.deb ... Unpacking libpkgconf3:amd64 (1.8.1-1) ... Selecting previously unselected package m4. Preparing to unpack .../archives/m4_1.4.19-3_amd64.deb ... Unpacking m4 (1.4.19-3) ... Selecting previously unselected package pkgconf-bin. Preparing to unpack .../pkgconf-bin_1.8.1-1_amd64.deb ... Unpacking pkgconf-bin (1.8.1-1) ... Selecting previously unselected package pkgconf:amd64. Preparing to unpack .../pkgconf_1.8.1-1_amd64.deb ... Unpacking pkgconf:amd64 (1.8.1-1) ... Selecting previously unselected package pkg-config:amd64. Preparing to unpack .../pkg-config_1.8.1-1_amd64.deb ... Unpacking pkg-config:amd64 (1.8.1-1) ... Setting up m4 (1.4.19-3) ... Setting up libpkgconf3:amd64 (1.8.1-1) ... Setting up pkgconf-bin (1.8.1-1) ... Setting up pkgconf:amd64 (1.8.1-1) ... Setting up pkg-config:amd64 (1.8.1-1) ... Processing triggers for libc-bin (2.36-9+deb12u3) ... 2024-01-29 19:11.44 ---> using "d64ddc7053307a6e5bac376e2af0af138c2728532db1941a0e2c7ed3dcb6923f" from cache /home/opam: (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "opam pin -ny https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 && opam depext -iy voodoo-prep")) [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo: git] [voodoo] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 This will pin the following packages: voodoo-prep, voodoo-lib, voodoo-gen, voodoo-do. Continue? [Y/n] y Package voodoo-prep does not exist, create as a NEW package? [Y/n] y [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev: git] [voodoo-prep.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 voodoo-prep is now pinned to git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 (version ~dev) Package voodoo-lib does not exist, create as a NEW package? [Y/n] y [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev: git] [voodoo-lib.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 voodoo-lib is now pinned to git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 (version ~dev) Package voodoo-gen does not exist, create as a NEW package? [Y/n] y [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev: git] [voodoo-gen.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 voodoo-gen is now pinned to git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 (version ~dev) Package voodoo-do does not exist, create as a NEW package? [Y/n] y [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev: git] [voodoo-do.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 voodoo-do is now pinned to git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 (version ~dev) # Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=debian, os-family=debian # No extra OS packages requirements found. # All required OS packages found. # Now letting opam install the packages <><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><> [voodoo-prep.~dev] no changes from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 The following actions will be performed: - install ocamlbuild 0.14.3 [required by bos] - install cmdliner 1.2.0 [required by voodoo-prep] - install dune 3.13.0 [required by voodoo-prep] - install ocamlfind 1.9.6 [required by bos] - install seq base [required by re] - install stdlib-shims 0.3.0 [required by ocamlgraph] - install opam-file-format 2.1.6 [required by opam-format] - install cppo 1.6.9 [required by opam-core] - install topkg 1.0.7 [required by bos] - install re 1.11.0 [required by opam-format] - install ocamlgraph 2.1.0 [required by opam-core] - install rresult 0.7.0 [required by bos] - install fmt 0.9.0 [required by bos] - install astring 0.8.5 [required by bos] - install opam-core 2.1.5 [required by opam-format] - install logs 0.7.0 [required by bos] - install fpath 0.7.3 [required by voodoo-prep] - install opam-format 2.1.5 [required by voodoo-prep] - install bos 0.2.1 [required by voodoo-prep] - install voodoo-prep ~dev* ===== 20 to install ===== <><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><> [astring.0.8.5] found in cache [bos.0.2.1] found in cache [cmdliner.1.2.0] found in cache [cppo.1.6.9] found in cache [dune.3.13.0] found in cache [fmt.0.9.0] found in cache [fpath.0.7.3] found in cache [logs.0.7.0] found in cache [ocamlbuild.0.14.3] found in cache [ocamlfind.1.9.6] found in cache [ocamlgraph.2.1.0] found in cache [opam-core.2.1.5] found in cache [opam-file-format.2.1.6] found in cache [opam-format.2.1.5] found in cache [re.1.11.0] found in cache [rresult.0.7.0] found in cache [stdlib-shims.0.3.0] found in cache [topkg.1.0.7] found in cache [voodoo-prep.~dev] synchronised from git+https://github.com/ocaml-doc/voodoo.git#67ccabec49b5f4d24147839291fcae7c19d3e8c9 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> installed seq.base -> installed cmdliner.1.2.0 -> installed ocamlfind.1.9.6 -> installed ocamlbuild.0.14.3 -> installed topkg.1.0.7 -> installed rresult.0.7.0 -> installed fmt.0.9.0 -> installed astring.0.8.5 -> installed fpath.0.7.3 -> installed logs.0.7.0 -> installed dune.3.13.0 -> installed bos.0.2.1 -> installed stdlib-shims.0.3.0 -> installed opam-file-format.2.1.6 -> installed re.1.11.0 -> installed cppo.1.6.9 -> installed ocamlgraph.2.1.0 -> installed opam-core.2.1.5 -> installed opam-format.2.1.5 -> installed voodoo-prep.~dev Done. # Run eval $(opam env) to update the current shell environment 2024-01-29 19:11.44 ---> using "d95d2426ec6638d4946232810cc7377b78e0b12578cf93755f6aecdc254fcd78" from cache /home/opam: (run (shell "cp $(opam config var bin)/voodoo-prep /home/opam")) 2024-01-29 19:11.44 ---> using "200b9dc9bbc6b05727626f4e73227cdcfa87e5df3b69dfe480b404d6323d60f8" from cache 2024-01-29 19:11.44 --> finished "tools" (from ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef) Unable to find image 'ocaml/opam:debian-12-ocaml-4.14@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef' locally docker.io/ocaml/opam@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef: Pulling from ocaml/opam 82e8c0c7d92b: Pulling fs layer 82e8c0c7d92b: Verifying Checksum 82e8c0c7d92b: Download complete 82e8c0c7d92b: Pull complete Digest: sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef Status: Downloaded newer image for ocaml/opam@sha256:8e390dbf29f7a115e5c8098ffb1a3c7234a873cf738a5ae22f3a4846122db9ef 2024-01-29 19:11.44 ---> using "1f16aa8fbc1a229ca02cdf7d8b4234eb4608a9074cec5292a9e72517b48fb577" from cache /: (user (uid 1000) (gid 1000)) /: (workdir /home/opam) /home/opam: (run (shell "sudo chown opam:opam /home/opam")) 2024-01-29 19:11.44 ---> using "258ae3900365106d3b475f7327e1977f1a9ae54d4b6cd6e024f1ed5ef4f3381c" from cache /home/opam: (run (shell "sudo mkdir /src")) 2024-01-29 19:11.44 ---> using "50a061015e57b489daec5893a083c81b93ec0b29b89dbcf9b55da6d4003431c6" from cache /home/opam: (copy (src packages) (dst /src/packages)) 2024-01-29 19:11.45 ---> using "c760f095cd91f380e8b56dca3d83924015872d1815e0d677d17a4cf4936368f0" from cache /home/opam: (copy (src repo) (dst /src/repo)) 2024-01-29 19:11.45 ---> using "d0bbe6c2db9808e7eddb4ffba6c49d26bff58aa61ec83f20e5630e6879696066" from cache /home/opam: (run (network host) (shell "sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam && opam init --reinit -ni")) Configuring from /home/opam/.opamrc and then from built-in defaults. Checking for available remotes: rsync and local, git. - you won't be able to use mercurial repositories unless you install the hg command on your system. - you won't be able to use darcs repositories unless you install the darcs command on your system. This version of opam requires an update to the layout of /home/opam/.opam from version 2.0 to version 2.1, which can't be reverted. You may want to back it up before going further. Continue? [Y/n] y Format upgrade done. <><> Updating repositories ><><><><><><><><><><><><><><><><><><><><><><><><><><> [default] synchronised from file:///home/opam/opam-repository 2024-01-29 19:11.45 ---> using "682fb30d9437994e091a3c4e1fcedffc4634900d13f2bd409830c4100dd57161" from cache /home/opam: (run (shell "opam repo remove default && opam repo add opam /src")) Repositories removed from the selections of switch 4.14. Use '--all' to forget about them altogether. [opam] Initialised [NOTE] Repository opam has been added to the selections of switch 4.14 only. Run `opam repository add opam --all-switches|--set-default' to use it in all existing switches, or in newly created switches, respectively. 2024-01-29 19:11.45 ---> using "9f82566f7239f462cee5f17110815e43c6d3ca7816f7448f13b01fb7bcf50e83" from cache /home/opam: (copy (from (build tools)) (src /home/opam/voodoo-prep) (dst /home/opam/)) 2024-01-29 19:11.45 ---> using "e2f3248260b96748ed9565f6b820205cf221dcc1b96d9f3eccf243a894156cba" from cache /home/opam: (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "opam install ocamlfind.1.9.6")) The following actions will be performed: - install ocamlfind 1.9.6 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> retrieved ocamlfind.1.9.6 (cached) -> installed ocamlfind.1.9.6 Done. # Run eval $(opam env) to update the current shell environment 2024-01-29 19:12.01 ---> saved as "1c8e63a972812a981c4602f3c592fcc5368d2342ff3413708f2628743687c60d" /home/opam: (env DUNE_CACHE disabled) /home/opam: (env DUNE_CACHE_TRANSPORT direct) /home/opam: (env DUNE_CACHE_DUPLICATION copy) /home/opam: (run (cache (opam-archives (target /home/opam/.opam/download-cache)) (opam-dune-cache (target /home/opam/.cache/dune))) (network host) (shell "(sudo apt update) && ((opam depext -viy z3_tptp.4.8.13 zarith.1.13 z3.4.8.13 ocamlfind.1.9.6 conf-python-3.9.0.0 conf-gmp.4 conf-g++.1.0 conf-c++.1.0 2>&1 | tee ~/opam.err.log) || echo 'Failed to install all packages')")) WARNING: apt does not have a stable CLI interface. Use with caution in scripts. Hit:1 http://deb.debian.org/debian bookworm InRelease Get:2 http://deb.debian.org/debian bookworm-updates InRelease [52.1 kB] Get:3 http://deb.debian.org/debian-security bookworm-security InRelease [48.0 kB] Get:4 http://deb.debian.org/debian-security bookworm-security/main amd64 Packages [134 kB] Fetched 234 kB in 0s (843 kB/s) Reading package lists... Building dependency tree... Reading state information... All packages are up to date. Opam plugin "depext" may require upgrading/reinstalling. Reinstall the plugin on the current switch? [Y/n] y The following actions will be performed: - recompile opam-depext 1.2.1-1 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> -> retrieved opam-depext.1.2.1-1 (cached) -> removed opam-depext.1.2.1-1 -> installed opam-depext.1.2.1-1 Done. <><> opam-depext.1.2.1-1 installed successfully <><><><><><><><><><><><><><><><> => opam-depext is unnecessary when used with opam >= 2.1. Please use opam install directly instead # Run eval $(opam env) to update the current shell environment <><> Carrying on to "opam depext -viy z3_tptp.4.8.13 zarith.1.13 z3.4.8.13 ocamlfind.1.9.6 conf-python-3.9.0.0 conf-gmp.4 conf-g++.1.0 conf-c++.1.0" You are using opam 2.1+, where external dependency handling has been integrated: consider calling opam directly, the 'depext' plugin interface is provided for backwards compatibility only # Detecting depexts using vars: arch=x86_64, os=linux, os-distribution=debian, os-family=debian # The following system packages are needed: g++ libgmp-dev python3 python3-distutils [NOTE] Package ocamlfind is already installed (current version is 1.9.6). The following actions will be performed: - install conf-python-3 9.0.0 - install conf-gmp 4 - install conf-g++ 1.0 - install conf-c++ 1.0 - install zarith 1.13 - install z3 4.8.13 - install z3_tptp 4.8.13 ===== 7 to install ===== The following system packages will first need to be installed: libgmp-dev python3 python3-distutils <><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><> Let opam run your package manager to install the required system packages? (answer 'n' for other options) [Y/n] y + /usr/bin/sudo "apt-get" "install" "-qq" "-yy" "libgmp-dev" "python3" "python3-distutils" - debconf: delaying package configuration, since apt-utils is not installed - Selecting previously unselected package libpython3.11-minimal:amd64. - (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 18743 files and directories currently installed.) - Preparing to unpack .../libpython3.11-minimal_3.11.2-6_amd64.deb ... - Unpacking libpython3.11-minimal:amd64 (3.11.2-6) ... - Selecting previously unselected package python3.11-minimal. - Preparing to unpack .../python3.11-minimal_3.11.2-6_amd64.deb ... - Unpacking python3.11-minimal (3.11.2-6) ... - Setting up libpython3.11-minimal:amd64 (3.11.2-6) ... - Setting up python3.11-minimal (3.11.2-6) ... - Selecting previously unselected package python3-minimal. - (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19050 files and directories currently installed.) - Preparing to unpack .../python3-minimal_3.11.2-1+b1_amd64.deb ... - Unpacking python3-minimal (3.11.2-1+b1) ... - Selecting previously unselected package media-types. - Preparing to unpack .../media-types_10.0.0_all.deb ... - Unpacking media-types (10.0.0) ... - Selecting previously unselected package libpython3.11-stdlib:amd64. - Preparing to unpack .../libpython3.11-stdlib_3.11.2-6_amd64.deb ... - Unpacking libpython3.11-stdlib:amd64 (3.11.2-6) ... - Selecting previously unselected package python3.11. - Preparing to unpack .../python3.11_3.11.2-6_amd64.deb ... - Unpacking python3.11 (3.11.2-6) ... - Selecting previously unselected package libpython3-stdlib:amd64. - Preparing to unpack .../libpython3-stdlib_3.11.2-1+b1_amd64.deb ... - Unpacking libpython3-stdlib:amd64 (3.11.2-1+b1) ... - Setting up python3-minimal (3.11.2-1+b1) ... - Selecting previously unselected package python3. - (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19460 files and directories currently installed.) - Preparing to unpack .../python3_3.11.2-1+b1_amd64.deb ... - Unpacking python3 (3.11.2-1+b1) ... - Selecting previously unselected package libgmpxx4ldbl:amd64. - Preparing to unpack .../libgmpxx4ldbl_2%3a6.2.1+dfsg1-1.1_amd64.deb ... - Unpacking libgmpxx4ldbl:amd64 (2:6.2.1+dfsg1-1.1) ... - Selecting previously unselected package libgmp-dev:amd64. - Preparing to unpack .../libgmp-dev_2%3a6.2.1+dfsg1-1.1_amd64.deb ... - Unpacking libgmp-dev:amd64 (2:6.2.1+dfsg1-1.1) ... - Selecting previously unselected package python3-lib2to3. - Preparing to unpack .../python3-lib2to3_3.11.2-3_all.deb ... - Unpacking python3-lib2to3 (3.11.2-3) ... - Selecting previously unselected package python3-distutils. - Preparing to unpack .../python3-distutils_3.11.2-3_all.deb ... - Unpacking python3-distutils (3.11.2-3) ... - Setting up media-types (10.0.0) ... - Setting up libpython3.11-stdlib:amd64 (3.11.2-6) ... - Setting up libgmpxx4ldbl:amd64 (2:6.2.1+dfsg1-1.1) ... - Setting up libpython3-stdlib:amd64 (3.11.2-1+b1) ... - Setting up python3.11 (3.11.2-6) ... - Setting up libgmp-dev:amd64 (2:6.2.1+dfsg1-1.1) ... - Setting up python3 (3.11.2-1+b1) ... - running python rtupdate hooks for python3.11... - running python post-rtupdate hooks for python3.11... - Setting up python3-lib2to3 (3.11.2-3) ... - Setting up python3-distutils (3.11.2-3) ... - Processing triggers for libc-bin (2.36-9+deb12u3) ... <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><> Processing 5/21: Processing 6/21: Processing 7/21: Processing 8/21: [conf-c++: c++] Processing 9/21: [conf-c++: c++] [conf-g++: g++] Processing 10/21: [conf-c++: c++] [conf-g++: g++] [conf-gmp: sh] Processing 11/21: [conf-c++: c++] [conf-g++: g++] [conf-gmp: sh] [conf-python-3: python3 test.py] -> retrieved z3.4.8.13 (cached) -> retrieved z3_tptp.4.8.13 (cached) -> retrieved zarith.1.13 (cached) - c++ (Debian 12.2.0-14) 12.2.0 - Copyright (C) 2022 Free Software Foundation, Inc. - This is free software; see the source for copying conditions. There is NO - warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. - -> compiled conf-c++.1.0 Processing 11/21: [conf-g++: g++] [conf-gmp: sh] [conf-python-3: python3 test.py] -> installed conf-c++.1.0 Processing 12/21: [conf-g++: g++] [conf-gmp: sh] [conf-python-3: python3 test.py] - g++ (Debian 12.2.0-14) 12.2.0 - Copyright (C) 2022 Free Software Foundation, Inc. - This is free software; see the source for copying conditions. There is NO - warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. - -> compiled conf-g++.1.0 Processing 12/21: [conf-gmp: sh] [conf-python-3: python3 test.py] -> installed conf-g++.1.0 Processing 13/21: [conf-gmp: sh] [conf-python-3: python3 test.py] - + cc -c -I/usr/local/include test.c -> compiled conf-gmp.4 Processing 13/21: [conf-python-3: python3 test.py] -> installed conf-gmp.4 Processing 14/21: [conf-python-3: python3 test.py] Processing 15/21: [conf-python-3: python3 test.py] [zarith: ./configure] - python-3 OK -> compiled conf-python-3.9.0.0 Processing 15/21: [zarith: ./configure] -> installed conf-python-3.9.0.0 Processing 16/21: [zarith: ./configure] + /home/opam/.opam/4.14/.opam-switch/build/zarith.1.13/./configure (CWD=/home/opam/.opam/4.14/.opam-switch/build/zarith.1.13) - binary ocaml: found in /home/opam/.opam/4.14/bin - binary ocamlc: found in /home/opam/.opam/4.14/bin - binary ocamldep: found in /home/opam/.opam/4.14/bin - binary ocamlmklib: found in /home/opam/.opam/4.14/bin - binary ocamldoc: found in /home/opam/.opam/4.14/bin - binary ocamlopt: found in /home/opam/.opam/4.14/bin - checking compilation with ocamlc -O3 -Wall -Wextra : working - include caml/mlvalues.h: found - library dynlink.cmxa: found - binary ocamlfind: found in /home/opam/.opam/4.14/bin - OCaml's word size is 64 - include gmp.h: found - library gmp: found - OCaml supports -bin-annot to produce documentation - - detected configuration: - - native-code: yes - dynamic linking: yes - defines: -DHAS_GMP - includes: -I/home/opam/.opam/4.14/lib/ocaml - libraries: -lgmp - linker options: - C options: -O3 -Wall -Wextra - installation path: /home/opam/.opam/4.14/lib - installation method findlib - - configuration successful! - now type "make" to build - then type "make install" or "sudo make install" to install Processing 16/21: [zarith: make] + /usr/bin/make (CWD=/home/opam/.opam/4.14/.opam-switch/build/zarith.1.13) - (echo "let"; grep "version" META | head -1) > zarith_version.ml - ocamldep zarith_version.ml z.ml q.ml big_int_Z.ml z.mli q.mli big_int_Z.mli > depend - ocamlc -g -I +compiler-libs -bin-annot -c zarith_version.ml - ocamlc -g -I +compiler-libs -bin-annot -c z.mli - ocamlc -g -I +compiler-libs -bin-annot -c z.ml - ocamlc -g -I +compiler-libs -bin-annot -c q.mli - ocamlc -g -I +compiler-libs -bin-annot -c q.ml - ocamlc -g -I +compiler-libs -bin-annot -c big_int_Z.mli - ocamlc -g -I +compiler-libs -bin-annot -c big_int_Z.ml - ocamlmklib -g -failsafe -o zarith zarith_version.cmo z.cmo q.cmo big_int_Z.cmo -lgmp - ocamlc -ccopt "-I/home/opam/.opam/4.14/lib/ocaml -DHAS_GMP -O3 -Wall -Wextra " -c caml_z.c - ocamlmklib -g -failsafe -o zarith caml_z.o -lgmp - ocamlc -g -I +compiler-libs -bin-annot -c zarith_top.ml - ocamlc -g -o zarith_top.cma -a zarith_top.cmo - ocamlopt -g -I +compiler-libs -c zarith_version.ml - ocamlopt -g -I +compiler-libs -c z.ml - ocamlopt -g -I +compiler-libs -c q.ml - ocamlopt -g -I +compiler-libs -c big_int_Z.ml - ocamlmklib -g -failsafe -o zarith zarith_version.cmx z.cmx q.cmx big_int_Z.cmx -lgmp - ocamlopt -shared -o zarith.cmxs -I . zarith.cmxa -linkall -> compiled zarith.1.13 Processing 17/21: [zarith: make install] + /usr/bin/make "install" (CWD=/home/opam/.opam/4.14/.opam-switch/build/zarith.1.13) - ocamlfind install -destdir "/home/opam/.opam/4.14/lib" zarith META zarith.cma libzarith.a z.cmi q.cmi big_int_Z.cmi zarith_top.cma z.mli zarith.cmxa zarith_version.cmx z.cmx q.cmx big_int_Z.cmx zarith.cmxs zarith.h q.mli big_int_Z.mli zarith.a z.cmti q.cmti big_int_Z.cmti -optional dllzarith.so - Installed /home/opam/.opam/4.14/lib/zarith/big_int_Z.cmti - Installed /home/opam/.opam/4.14/lib/zarith/q.cmti - Installed /home/opam/.opam/4.14/lib/zarith/z.cmti - Installed /home/opam/.opam/4.14/lib/zarith/zarith.a - Installed /home/opam/.opam/4.14/lib/zarith/big_int_Z.mli - Installed /home/opam/.opam/4.14/lib/zarith/q.mli - Installed /home/opam/.opam/4.14/lib/zarith/zarith.h - Installed /home/opam/.opam/4.14/lib/zarith/zarith.cmxs - Installed /home/opam/.opam/4.14/lib/zarith/big_int_Z.cmx - Installed /home/opam/.opam/4.14/lib/zarith/q.cmx - Installed /home/opam/.opam/4.14/lib/zarith/z.cmx - Installed /home/opam/.opam/4.14/lib/zarith/zarith_version.cmx - Installed /home/opam/.opam/4.14/lib/zarith/zarith.cmxa - Installed /home/opam/.opam/4.14/lib/zarith/z.mli - Installed /home/opam/.opam/4.14/lib/zarith/zarith_top.cma - Installed /home/opam/.opam/4.14/lib/zarith/big_int_Z.cmi - Installed /home/opam/.opam/4.14/lib/zarith/q.cmi - Installed /home/opam/.opam/4.14/lib/zarith/z.cmi - Installed /home/opam/.opam/4.14/lib/zarith/libzarith.a - Installed /home/opam/.opam/4.14/lib/zarith/zarith.cma - Installed /home/opam/.opam/4.14/lib/stublibs/dllzarith.so - Installed /home/opam/.opam/4.14/lib/stublibs/dllzarith.so.owner - ocamlfind: [WARNING] You have installed DLLs but the directory /home/opam/.opam/4.14/lib/stublibs is not mentioned in ld.conf - Installed /home/opam/.opam/4.14/lib/zarith/META -> installed zarith.1.13 Processing 18/21: [z3: python3] + /usr/bin/python3 "scripts/mk_make.py" "--ml" (CWD=/home/opam/.opam/4.14/.opam-switch/build/z3.4.8.13) - opt = --ml, arg = - New component: 'util' - New component: 'polynomial' - New component: 'interval' - New component: 'dd' - New component: 'simplex' - New component: 'hilbert' - New component: 'automata' - New component: 'realclosure' - New component: 'subpaving' - New component: 'ast' - New component: 'euf' - New component: 'params' - New component: 'smt_params' - New component: 'grobner' - New component: 'sat' - New component: 'nlsat' - New component: 'lp' - New component: 'rewriter' - New component: 'macros' - New component: 'normal_forms' - New component: 'model' - New component: 'tactic' - New component: 'substitution' - New component: 'parser_util' - New component: 'proofs' - New component: 'solver' - New component: 'cmd_context' - New component: 'smt2parser' - New component: 'pattern' - New component: 'solver_assertions' - New component: 'aig_tactic' - New component: 'ackermannization' - New component: 'fpa' - New component: 'bit_blaster' - New component: 'core_tactics' - New component: 'arith_tactics' - New component: 'mbp' - New component: 'sat_smt' - New component: 'sat_tactic' - New component: 'nlsat_tactic' - New component: 'subpaving_tactic' - New component: 'proto_model' - New component: 'smt' - New component: 'bv_tactics' - New component: 'fuzzing' - New component: 'smt_tactic' - New component: 'sls_tactic' - New component: 'qe' - New component: 'sat_solver' - New component: 'fd_solver' - New component: 'muz' - New component: 'dataflow' - New component: 'transforms' - New component: 'rel' - New component: 'spacer' - New component: 'clp' - New component: 'tab' - New component: 'ddnf' - New component: 'bmc' - New component: 'fp' - New component: 'smtlogic_tactics' - New component: 'ufbv_tactic' - New component: 'fpa_tactics' - New component: 'portfolio' - New component: 'opt' - New component: 'api' - New component: 'extra_cmds' - New component: 'shell' - New component: 'test' - New component: 'api_dll' - New component: 'dotnet' - New component: 'java' - New component: 'ml' - New component: 'cpp' - Python bindings directory was detected. - New component: 'python' - New component: 'python_install' - New component: 'js' - New component: 'cpp_example' - New component: 'z3_tptp' - New component: 'c_example' - New component: 'maxsat' - New component: 'dotnet_example' - New component: 'java_example' - New component: 'ml_example' - New component: 'py_example' - Generating src/util/z3_version.h from src/util/z3_version.h.in - Generated 'src/util/z3_version.h' - Generated 'src/tactic/tactic_params.hpp' - Generated 'src/tactic/smtlogics/qfufbv_tactic_params.hpp' - Generated 'src/tactic/sls/sls_params.hpp' - Generated 'src/solver/solver_params.hpp' - Generated 'src/solver/parallel_params.hpp' - Generated 'src/solver/combined_solver_params.hpp' - Generated 'src/smt/params/smt_params_helper.hpp' - Generated 'src/sat/sat_simplifier_params.hpp' - Generated 'src/sat/sat_scc_params.hpp' - Generated 'src/sat/sat_params.hpp' - Generated 'src/sat/sat_asymm_branch_params.hpp' - Generated 'src/parsers/util/parser_params.hpp' - Generated 'src/params/seq_rewriter_params.hpp' - Generated 'src/params/rewriter_params.hpp' - Generated 'src/params/poly_rewriter_params.hpp' - Generated 'src/params/pattern_inference_params_helper.hpp' - Generated 'src/params/fpa_rewriter_params.hpp' - Generated 'src/params/fpa2bv_rewriter_params.hpp' - Generated 'src/params/bv_rewriter_params.hpp' - Generated 'src/params/bool_rewriter_params.hpp' - Generated 'src/params/array_rewriter_params.hpp' - Generated 'src/params/arith_rewriter_params.hpp' - Generated 'src/opt/opt_params.hpp' - Generated 'src/nlsat/nlsat_params.hpp' - Generated 'src/muz/base/fp_params.hpp' - Generated 'src/model/model_params.hpp' - Generated 'src/model/model_evaluator_params.hpp' - Generated 'src/math/realclosure/rcf_params.hpp' - Generated 'src/math/polynomial/algebraic_params.hpp' - Generated 'src/ast/pp_params.hpp' - Generated 'src/ast/normal_forms/nnf_params.hpp' - Generated 'src/ackermannization/ackermannize_bv_tactic_params.hpp' - Generated 'src/ackermannization/ackermannization_params.hpp' - Generated 'src/ast/pattern/database.h' - Component api - Component portfolio - Component smtlogic_tactics - Component ackermannization - Component model - Component rewriter - Component ast - Component util - Component polynomial - Component automata - Component params - Component macros - Component solver - Component tactic - Component proofs - Component sat_solver - Component core_tactics - Component normal_forms - Component pattern - Component smt2parser - Component cmd_context - Component parser_util - Component aig_tactic - Component bv_tactics - Component bit_blaster - Component arith_tactics - Component sat - Component dd - Component interval - Component grobner - Component simplex - Component sat_tactic - Component sat_smt - Component euf - Component smt_params - Component fpa - Component mbp - Component lp - Component nlsat - Component nlsat_tactic - Component smt_tactic - Component smt - Component proto_model - Component solver_assertions - Component substitution - Component fp - Component muz - Component qe - Component clp - Component transforms - Component hilbert - Component dataflow - Component tab - Component rel - Component bmc - Component fd_solver - Component ddnf - Component spacer - Component ufbv_tactic - Component fpa_tactics - Component sls_tactic - Component subpaving_tactic - Component subpaving - Component realclosure - Component opt - Component extra_cmds - Component shell - Generated 'src/shell/install_tactic.cpp' - Component api - Component portfolio - Component smtlogic_tactics - Component ackermannization - Component model - Component rewriter - Component ast - Component util - Component polynomial - Component automata - Component params - Component macros - Component solver - Component tactic - Component proofs - Component sat_solver - Component core_tactics - Component normal_forms - Component pattern - Component smt2parser - Component cmd_context - Component parser_util - Component aig_tactic - Component bv_tactics - Component bit_blaster - Component arith_tactics - Component sat - Component dd - Component interval - Component grobner - Component simplex - Component sat_tactic - Component sat_smt - Component euf - Component smt_params - Component fpa - Component mbp - Component lp - Component nlsat - Component nlsat_tactic - Component smt_tactic - Component smt - Component proto_model - Component solver_assertions - Component substitution - Component fp - Component muz - Component qe - Component clp - Component transforms - Component hilbert - Component dataflow - Component tab - Component rel - Component bmc - Component fd_solver - Component ddnf - Component spacer - Component ufbv_tactic - Component fpa_tactics - Component sls_tactic - Component subpaving_tactic - Component subpaving - Component realclosure - Component opt - Component fuzzing - Component test - Generated 'src/test/install_tactic.cpp' - Component api - Component portfolio - Component smtlogic_tactics - Component ackermannization - Component model - Component rewriter - Component ast - Component util - Component polynomial - Component automata - Component params - Component macros - Component solver - Component tactic - Component proofs - Component sat_solver - Component core_tactics - Component normal_forms - Component pattern - Component smt2parser - Component cmd_context - Component parser_util - Component aig_tactic - Component bv_tactics - Component bit_blaster - Component arith_tactics - Component sat - Component dd - Component interval - Component grobner - Component simplex - Component sat_tactic - Component sat_smt - Component euf - Component smt_params - Component fpa - Component mbp - Component lp - Component nlsat - Component nlsat_tactic - Component smt_tactic - Component smt - Component proto_model - Component solver_assertions - Component substitution - Component fp - Component muz - Component qe - Component clp - Component transforms - Component hilbert - Component dataflow - Component tab - Component rel - Component bmc - Component fd_solver - Component ddnf - Component spacer - Component ufbv_tactic - Component fpa_tactics - Component sls_tactic - Component subpaving_tactic - Component subpaving - Component realclosure - Component opt - Component extra_cmds - Component api_dll - Generated 'src/api/dll/install_tactic.cpp' - Generated 'src/shell/mem_initializer.cpp' - Generated 'src/test/mem_initializer.cpp' - Generated 'src/api/dll/mem_initializer.cpp' - Generated 'src/shell/gparams_register_modules.cpp' - Generated 'src/test/gparams_register_modules.cpp' - Generated 'src/api/dll/gparams_register_modules.cpp' - Generated 'src/api/python/z3/z3consts.py - Generated 'src/api/api_log_macros.h' - Generated 'src/api/api_log_macros.cpp' - Generated 'src/api/api_commands.cpp' - Generated 'src/api/python/z3/z3core.py' - Generated "src/api/ml/z3native.ml" - Generated "src/api/ml/z3native_stubs.c" - Listing 'src/api/python/z3'... - Compiling 'src/api/python/z3/__init__.py'... - Compiling 'src/api/python/z3/z3.py'... - Compiling 'src/api/python/z3/z3consts.py'... - Compiling 'src/api/python/z3/z3core.py'... - Compiling 'src/api/python/z3/z3num.py'... - Compiling 'src/api/python/z3/z3poly.py'... - Compiling 'src/api/python/z3/z3printer.py'... - Compiling 'src/api/python/z3/z3rcf.py'... - Compiling 'src/api/python/z3/z3types.py'... - Compiling 'src/api/python/z3/z3util.py'... - Generated python bytecode - Copied 'z3core.py' - Copied 'z3consts.py' - Copied 'z3util.py' - Copied 'z3types.py' - Copied 'z3rcf.py' - Copied 'z3printer.py' - Copied 'z3poly.py' - Copied 'z3num.py' - Copied 'z3.py' - Copied '__init__.py' - Copied 'z3util.cpython-311.pyc' - Copied 'z3types.cpython-311.pyc' - Copied 'z3rcf.cpython-311.pyc' - Copied 'z3printer.cpython-311.pyc' - Copied 'z3poly.cpython-311.pyc' - Copied 'z3num.cpython-311.pyc' - Copied 'z3core.cpython-311.pyc' - Copied 'z3consts.cpython-311.pyc' - Copied 'z3.cpython-311.pyc' - Copied '__init__.cpython-311.pyc' - Testing ocamlc... - Testing ocamlopt... - Finding OCAML_LIB... - OCAML_LIB=/home/opam/.opam/4.14/lib/ocaml - Testing ocamlfind... - Generated "src/api/ml/z3enums.ml" - Testing ar... - Testing g++... - Testing gcc... - Testing floating point support... - Host platform: Linux - C++ Compiler: g++ - C Compiler : gcc - Archive Tool: ar - Arithmetic: internal - Prefix: /usr - 64-bit: True - FP math: SSE2-GCC - Python pkg dir: /usr/lib/python3/dist-packages - Python version: 3.11 - OCaml Compiler: ocamlc - OCaml Find tool: ocamlfind - OCaml Native: ocamlopt - OCaml Library: /home/opam/.opam/4.14/lib/ocaml - Writing build/Makefile - Generating build/api/ml/META from src/api/ml/META.in - Copied Z3Py example 'visitor.py' to 'build/python' - Copied Z3Py example 'union_sort.py' to 'build/python' - Copied Z3Py example 'trafficjam.py' to 'build/python' - Copied Z3Py example 'socrates.py' to 'build/python' - Copied Z3Py example 'rc2.py' to 'build/python' - Copied Z3Py example 'parallel.py' to 'build/python' - Copied Z3Py example 'mini_quip.py' to 'build/python' - Copied Z3Py example 'mini_ic3.py' to 'build/python' - Copied Z3Py example 'hs.py' to 'build/python' - Copied Z3Py example 'example.py' to 'build/python' - Copied Z3Py example 'efsmt.py' to 'build/python' - Copied Z3Py example 'all_interval_series.py' to 'build/python' - Makefile was successfully generated. - compilation mode: Release - Type 'cd build; make' to build Z3 Processing 18/21: [z3: make build] + /usr/bin/make "-C" "build" "-j" "255" (CWD=/home/opam/.opam/4.14/.opam-switch/build/z3.4.8.13) - make: Entering directory '/home/opam/.opam/4.14/.opam-switch/build/z3.4.8.13/build' - src/smt/smt_statistics.cpp - src/util/luby.cpp - src/util/common_msgs.cpp - src/util/approx_nat.cpp - src/api/dll/dll.cpp - ocamlfind ocamlc -package zarith -i -I api/ml -c ../src/api/ml/z3enums.ml > api/ml/z3enums.mli - src/util/z3_exception.cpp - src/util/timeit.cpp - src/util/page.cpp - src/util/memory_manager.cpp - src/util/approx_set.cpp - ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3enums.cmi -c api/ml/z3enums.mli - ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3enums.cmo -c ../src/api/ml/z3enums.ml - src/util/util.cpp - src/util/timeout.cpp - src/util/stack.cpp - src/util/scoped_timer.cpp - src/util/scoped_ctrl_c.cpp - ocamlfind ocamlc -package zarith -i -I api/ml -c ../src/api/ml/z3native.ml > api/ml/z3native.mli - src/util/bit_util.cpp - ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3native.cmi -c api/ml/z3native.mli - src/shell/z3_log_frontend.cpp - src/api/api_commands.cpp - src/util/mpn.cpp - src/util/lbool.cpp - src/util/hash.cpp - src/util/fixed_bit_vector.cpp - ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3native.cmo -c ../src/api/ml/z3native.ml - cp ../src/api/ml/z3.mli api/ml/z3.mli - ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3.cmi -c api/ml/z3.mli - src/api/z3_replayer.cpp - src/solver/smt_logics.cpp - ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3.cmo -c ../src/api/ml/z3.ml - src/sat/sat_cutset.cpp - src/math/dd/dd_bdd.cpp - src/util/warning.cpp - src/util/trace.cpp - src/util/symbol.cpp - src/util/state_graph.cpp - src/util/smt2_util.cpp - src/util/small_object_allocator.cpp - src/util/rlimit.cpp - src/util/region.cpp - src/util/prime_generator.cpp - src/util/permutation.cpp - src/util/min_cut.cpp - src/util/debug.cpp - src/util/cmd_context_types.cpp - src/util/bit_vector.cpp - File "../src/api/ml/z3.ml", line 206, characters 16-34: - 206 | 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 - src/api/api_log_macros.cpp - src/api/api_log.cpp - src/sat/sat_watched.cpp - src/sat/sat_clause_use_list.cpp - src/sat/sat_clause.cpp - src/math/automata/automaton.cpp - src/math/simplex/bit_matrix.cpp - src/util/statistics.cpp - src/util/mpz.cpp - src/sat/sat_clause_set.cpp - src/math/realclosure/mpz_matrix.cpp - src/math/interval/interval_mpq.cpp - src/util/mpq_inf.cpp - src/util/mpq.cpp - src/util/mpfx.cpp - src/util/mpff.cpp - src/util/gparams.cpp - src/util/env_params.cpp - src/shell/mem_initializer.cpp - src/smt/old_interval.cpp - src/tactic/arith/linear_equation.cpp - src/sat/sat_config.cpp - src/smt/params/theory_str_params.cpp - src/smt/params/theory_seq_params.cpp - src/smt/params/theory_pb_params.cpp - src/smt/params/theory_bv_params.cpp - src/smt/params/theory_array_params.cpp - src/smt/params/theory_arith_params.cpp - src/smt/params/qi_params.cpp - src/smt/params/preprocessor_params.cpp - src/smt/params/dyn_ack_params.cpp - src/params/pattern_inference_params.cpp - src/math/realclosure/realclosure.cpp - src/math/dd/dd_pdd.cpp - src/math/interval/dep_intervals.cpp - src/util/sexpr.cpp - src/util/s_integer.cpp - src/util/rational.cpp - src/util/params.cpp - src/util/mpf.cpp - src/util/mpbq.cpp - src/util/inf_rational.cpp - src/util/inf_int_rational.cpp - src/util/hwf.cpp - ocamlfind ocamlopt -package zarith -I api/ml -o api/ml/z3enums.cmx -c ../src/api/ml/z3enums.ml - src/api/dll/mem_initializer.cpp - src/muz/spacer/spacer_matrix.cpp - src/tactic/arith/bound_propagator.cpp - src/math/lp/lp_utils.cpp - src/sat/sat_simplifier.cpp - src/sat/sat_scc.cpp - src/sat/sat_probing.cpp - src/sat/sat_prob.cpp - src/sat/sat_parallel.cpp - src/sat/sat_npn3_finder.cpp - src/sat/sat_mus.cpp - src/sat/sat_model_converter.cpp - src/sat/sat_lookahead.cpp - src/sat/sat_local_search.cpp - src/sat/sat_integrity_checker.cpp - src/sat/sat_gc.cpp - src/sat/sat_elim_vars.cpp - src/sat/sat_elim_eqs.cpp - src/sat/sat_drat.cpp - src/sat/sat_ddfw.cpp - src/sat/sat_cut_simplifier.cpp - src/sat/sat_cleaner.cpp - src/sat/sat_binspr.cpp - src/sat/sat_big.cpp - src/sat/sat_bcd.cpp - src/sat/sat_asymm_branch.cpp - src/sat/sat_anf_simplifier.cpp - src/sat/sat_aig_finder.cpp - src/sat/sat_aig_cuts.cpp - src/sat/dimacs.cpp - src/math/subpaving/subpaving_mpq.cpp - src/math/subpaving/subpaving_mpfx.cpp - src/math/subpaving/subpaving_mpff.cpp - src/math/subpaving/subpaving_mpf.cpp - src/math/subpaving/subpaving_hwf.cpp - src/math/subpaving/subpaving.cpp - src/math/hilbert/hilbert_basis.cpp - src/math/simplex/simplex.cpp - src/util/zstring.cpp - ocamlfind ocamlopt -package zarith -I api/ml -o api/ml/z3native.cmx -c ../src/api/ml/z3native.ml - src/util/inf_s_integer.cpp - src/muz/rel/tbv.cpp - src/muz/base/bind_variables.cpp - src/sat/smt/sat_dual_solver.cpp - src/ast/rewriter/func_decl_replace.cpp - src/sat/sat_xor_finder.cpp - src/sat/sat_solver.cpp - src/sat/sat_lut_finder.cpp - src/math/grobner/pdd_solver.cpp - src/math/grobner/pdd_simplifier.cpp - src/smt/params/smt_params.cpp - src/params/context_params.cpp - src/ast/used_vars.cpp - src/ast/special_relations_decl_plugin.cpp - src/ast/quantifier_stat.cpp - src/ast/num_occurs.cpp - src/ast/has_free_vars.cpp - src/ast/for_each_ast.cpp - src/ast/expr_map.cpp - src/ast/expr_functors.cpp - src/ast/display_dimacs.cpp - src/ast/ast_lt.cpp - src/math/simplex/model_based_opt.cpp - ocamlfind ocamlopt -package zarith -I api/ml -o api/ml/z3.cmx -c ../src/api/ml/z3.ml - src/math/polynomial/polynomial_cache.cpp - src/smt/uses_theory.cpp - File "../src/api/ml/z3.ml", line 206, characters 16-34: - 206 | 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 - src/smt/smt_value_sort.cpp - src/ackermannization/ackr_helper.cpp - src/cmd_context/tactic_manager.cpp - src/parsers/util/simple_parser.cpp - src/parsers/util/scanner.cpp - src/parsers/util/cost_parser.cpp - src/ast/rewriter/mk_extract_proc.cpp - src/ast/rewriter/datatype_rewriter.cpp - src/math/lp/lp_settings.cpp - src/math/lp/binary_heap_priority_queue.cpp - src/nlsat/nlsat_types.cpp - src/nlsat/nlsat_clause.cpp - src/ast/pp.cpp - src/ast/occurs.cpp - src/ast/macro_substitution.cpp - src/ast/func_decl_dependencies.cpp - src/ast/format.cpp - src/ast/for_each_expr.cpp - src/ast/expr_stat.cpp - src/ast/cost_evaluator.cpp - src/ast/ast_ll_pp.cpp - src/ast/act_cache.cpp - src/math/polynomial/rpolynomial.cpp - src/math/polynomial/polynomial.cpp - src/shell/main.cpp - src/smt/arith_eq_solver.cpp - src/model/struct_factory.cpp - src/ast/rewriter/ast_counter.cpp - src/math/lp/indexed_vector.cpp - src/math/lp/binary_heap_upair_queue.cpp - src/nlsat/nlsat_interval_set.cpp - src/ast/euf/euf_enode.cpp - src/ast/value_generator.cpp - src/math/polynomial/upolynomial.cpp - src/math/polynomial/sexpr2upolynomial.cpp - src/math/polynomial/algebraic_numbers.cpp - src/api/dll/gparams_register_modules.cpp - src/shell/gparams_register_modules.cpp - src/qe/qe_bv_plugin.cpp - src/model/model2expr.cpp - src/ast/normal_forms/nnf.cpp - src/ast/normal_forms/elim_term_ite.cpp - src/ast/rewriter/mk_simplified_app.cpp - src/ast/rewriter/fpa_rewriter.cpp - src/ast/rewriter/dl_rewriter.cpp - src/ast/rewriter/distribute_forall.cpp - src/ast/rewriter/bv_bounds.cpp - src/math/lp/nex_creator.cpp - src/math/lp/dense_matrix.cpp - src/nlsat/nlsat_solver.cpp - src/nlsat/nlsat_explain.cpp - src/nlsat/nlsat_evaluator.cpp - src/ast/shared_occs.cpp - src/ast/fpa_decl_plugin.cpp - src/ast/expr2var.cpp - src/ast/expr2polynomial.cpp - src/ast/ast_smt_pp.cpp - src/ast/arith_decl_plugin.cpp - src/math/polynomial/upolynomial_factorization.cpp - src/opt/pb_sls.cpp - src/muz/spacer/spacer_qe_project.cpp - src/muz/spacer/spacer_mev_array.cpp - src/muz/spacer/spacer_mbc.cpp - src/muz/base/dl_boogie_proof.cpp - src/qe/qe_mbp.cpp - src/qe/qe_dl_plugin.cpp - src/qe/qe_datatype_plugin.cpp - src/qe/qe_bool_plugin.cpp - src/qe/qe_array_plugin.cpp - src/qe/nlarith_util.cpp - src/smt/watch_list.cpp - src/smt/smt_literal.cpp - src/smt/smt_farkas_util.cpp - src/smt/smt_clause.cpp - src/smt/proto_model/proto_model.cpp - src/math/subpaving/tactic/expr2subpaving.cpp - src/qe/mbp/mbp_term_graph.cpp - src/qe/mbp/mbp_solve_plugin.cpp - src/qe/mbp/mbp_plugin.cpp - src/qe/mbp/mbp_datatypes.cpp - src/qe/mbp/mbp_arrays.cpp - src/qe/mbp/mbp_arith.cpp - src/tactic/arith/bv2real_rewriter.cpp - src/ast/fpa/fpa2bv_rewriter.cpp - src/ast/fpa/fpa2bv_converter.cpp - src/ast/fpa/bv2fpa_converter.cpp - src/ackermannization/lackr_model_constructor.cpp - src/ast/pattern/pattern_inference.cpp - src/cmd_context/pdecl.cpp - src/solver/check_logic.cpp - src/ast/proofs/proof_utils.cpp - src/ast/proofs/proof_checker.cpp - src/parsers/util/pattern_validation.cpp - src/ast/substitution/unifier.cpp - src/ast/substitution/substitution_tree.cpp - src/ast/substitution/substitution.cpp - src/ast/substitution/matcher.cpp - src/tactic/replace_proof_converter.cpp - src/tactic/equiv_proof_converter.cpp - src/model/value_factory.cpp - src/model/numeral_factory.cpp - src/model/model_v2_pp.cpp - src/model/model_pp.cpp - src/model/model_macro_solver.cpp - src/model/model_implicant.cpp - src/model/model_core.cpp - src/model/func_interp.cpp - src/model/datatype_factory.cpp - src/model/array_factory.cpp - src/ast/normal_forms/pull_quant.cpp - src/ast/normal_forms/defined_names.cpp - src/ast/macros/quasi_macros.cpp - src/ast/normal_forms/name_exprs.cpp - src/ast/macros/quantifier_macro_info.cpp - src/ast/macros/macro_util.cpp - src/ast/macros/macro_manager.cpp - src/ast/rewriter/var_subst.cpp - src/ast/rewriter/seq_skolem.cpp - src/ast/rewriter/seq_eq_solver.cpp - src/ast/rewriter/seq_axioms.cpp - src/ast/rewriter/rewriter.cpp - src/ast/rewriter/quant_hoist.cpp - src/ast/rewriter/push_app_ite.cpp - src/ast/rewriter/pb_rewriter.cpp - src/ast/rewriter/pb2bv_rewriter.cpp - src/ast/rewriter/maximize_ac_sharing.cpp - src/ast/rewriter/label_rewriter.cpp - src/ast/rewriter/inj_axiom.cpp - src/ast/rewriter/hoist_rewriter.cpp - src/ast/rewriter/factor_rewriter.cpp - src/ast/rewriter/factor_equivs.cpp - src/ast/rewriter/expr_safe_replace.cpp - src/ast/rewriter/expr_replacer.cpp - src/ast/rewriter/enum2bv_rewriter.cpp - src/ast/rewriter/elim_bounds.cpp - src/ast/rewriter/der.cpp - src/ast/rewriter/cached_var_subst.cpp - src/ast/rewriter/bv_rewriter.cpp - src/ast/rewriter/bv_elim.cpp - src/ast/rewriter/bool_rewriter.cpp - src/ast/rewriter/bit2int.cpp - src/ast/rewriter/array_rewriter.cpp - src/ast/rewriter/arith_rewriter.cpp - src/math/lp/matrix.cpp - src/math/lp/permutation_matrix.cpp - src/math/grobner/grobner.cpp - src/ast/euf/euf_etable.cpp - src/ast/euf/euf_egraph.cpp - src/ast/well_sorted.cpp - src/ast/static_features.cpp - src/ast/seq_decl_plugin.cpp - src/ast/pb_decl_plugin.cpp - src/ast/expr_substitution.cpp - src/ast/expr_abstract.cpp - src/ast/dl_decl_plugin.cpp - src/ast/decl_collector.cpp - src/ast/datatype_decl_plugin.cpp - src/ast/char_decl_plugin.cpp - src/ast/bv_decl_plugin.cpp - src/ast/ast_translation.cpp - src/ast/ast_util.cpp - src/ast/ast_smt2_pp.cpp - src/ast/ast_printer.cpp - src/ast/ast_pp_dot.cpp - src/ast/ast.cpp - src/ast/array_decl_plugin.cpp - src/tactic/ufbv/ufbv_rewriter.cpp - src/muz/spacer/spacer_sem_matcher.cpp - src/muz/spacer/spacer_antiunify.cpp - src/tactic/bv/bit_blaster_model_converter.cpp - src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp - src/ast/rewriter/bit_blaster/bit_blaster.cpp - src/ackermannization/ackr_model_converter.cpp - src/solver/check_sat_result.cpp - src/tactic/model_converter.cpp - src/tactic/horn_subsume_model_converter.cpp - src/tactic/generic_model_converter.cpp - src/model/model_smt2_pp.cpp - src/model/model_evaluator.cpp - src/model/model.cpp - src/ast/macros/macro_finder.cpp - src/ast/rewriter/seq_rewriter.cpp - src/math/lp/eta_matrix.cpp - src/ast/reg_decl_plugins.cpp - src/ast/recfun_decl_plugin.cpp - src/ast/ast_pp_util.cpp - src/tactic/fpa/fpa2bv_model_converter.cpp - src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp - src/muz/spacer/spacer_sym_mux.cpp - src/muz/spacer/spacer_proof_utils.cpp - src/muz/spacer/spacer_iuc_solver.cpp - src/muz/spacer/spacer_iuc_proof.cpp - src/muz/spacer/spacer_farkas_learner.cpp - src/muz/base/hnf.cpp - src/qe/qe_mbi.cpp - src/tactic/bv/bvarray2uf_rewriter.cpp - src/smt/theory_opt.cpp - src/smt/smt_implied_equalities.cpp - src/smt/smt_cg_table.cpp - src/smt/smt_almost_cg_table.cpp - src/smt/fingerprints.cpp - src/sat/smt/pb_constraint.cpp - src/sat/smt/atom2bool_var.cpp - src/tactic/arith/pb2bv_model_converter.cpp - src/tactic/arith/bv2int_rewriter.cpp - src/tactic/arith/bound_manager.cpp - src/tactic/core/collect_occs.cpp - src/ackermannization/lackr_model_converter_lazy.cpp - src/ackermannization/ackermannize_bv_model_converter.cpp - src/tactic/aig/aig.cpp - src/solver/assertions/asserted_formulas.cpp - src/solver/solver.cpp - src/solver/mus.cpp - src/solver/combined_solver.cpp - src/tactic/proof_converter.cpp - src/tactic/goal_util.cpp - src/tactic/goal_shared_occs.cpp - src/tactic/goal_num_occurs.cpp - src/tactic/goal.cpp - src/tactic/dependency_converter.cpp - src/ast/rewriter/value_sweep.cpp - src/ast/rewriter/th_rewriter.cpp - src/ast/rewriter/recfun_rewriter.cpp - src/math/lp/scaler.cpp - src/shell/drat_frontend.cpp - src/shell/dimacs_frontend.cpp - src/cmd_context/extra_cmds/subpaving_cmds.cpp - src/cmd_context/extra_cmds/polynomial_cmds.cpp - src/cmd_context/extra_cmds/dbg_cmds.cpp - src/opt/opt_pareto.cpp - src/tactic/portfolio/solver2lookahead.cpp - src/tactic/smtlogics/smt_tactic.cpp - src/muz/spacer/spacer_unsat_core_plugin.cpp - src/muz/spacer/spacer_unsat_core_learner.cpp - src/muz/spacer/spacer_manager.cpp - src/muz/spacer/spacer_legacy_mev.cpp - src/muz/spacer/spacer_legacy_mbp.cpp - src/muz/rel/doc.cpp - src/tactic/fd_solver/smtfd_solver.cpp - src/tactic/fd_solver/pb2bv_solver.cpp - src/tactic/fd_solver/fd_solver.cpp - src/tactic/fd_solver/bounded_int2bv_solver.cpp - src/tactic/fd_solver/enum2bv_solver.cpp - src/qe/qsat.cpp - src/qe/qe_cmd.cpp - src/qe/qe_arith_plugin.cpp - src/qe/nlqsat.cpp - src/tactic/sls/sls_engine.cpp - src/smt/smt_solver.cpp - src/smt/smt2_extra_cmds.cpp - src/nlsat/tactic/goal2nlsat.cpp - src/sat/smt/user_solver.cpp - src/sat/smt/sat_th.cpp - src/sat/smt/recfun_solver.cpp - src/sat/smt/pb_pb.cpp - src/sat/smt/euf_relevancy.cpp - src/sat/smt/euf_proof.cpp - src/sat/smt/euf_model.cpp - src/sat/smt/euf_invariant.cpp - src/sat/smt/euf_internalize.cpp - src/sat/smt/euf_ackerman.cpp - src/sat/smt/dt_solver.cpp - src/sat/smt/bv_solver.cpp - src/sat/smt/bv_invariant.cpp - src/sat/smt/bv_internalize.cpp - src/sat/smt/bv_delay_internalize.cpp - src/sat/smt/bv_ackerman.cpp - src/sat/smt/array_solver.cpp - src/sat/smt/array_model.cpp - src/sat/smt/array_internalize.cpp - src/sat/smt/array_diagnostics.cpp - src/sat/smt/array_axioms.cpp - src/tactic/arith/arith_bounds_tactic.cpp - src/tactic/arith/probe_arith.cpp - src/tactic/core/reduce_invertible_tactic.cpp - src/tactic/core/cofactor_elim_term_ite.cpp - src/ackermannization/lackr.cpp - src/ast/pattern/expr_pattern_match.cpp - src/parsers/smt2/marshal.cpp - src/cmd_context/simplify_cmd.cpp - src/cmd_context/parametric_cmd.cpp - src/cmd_context/eval_cmd.cpp - src/cmd_context/echo_tactic.cpp - src/cmd_context/cmd_util.cpp - src/cmd_context/cmd_context_to_goal.cpp - src/cmd_context/cmd_context.cpp - src/cmd_context/basic_cmds.cpp - src/solver/tactic2solver.cpp - src/solver/solver_pool.cpp - src/solver/solver_na2as.cpp - src/solver/solver2tactic.cpp - src/tactic/tactic.cpp - src/tactic/probe.cpp - src/math/lp/square_sparse_matrix.cpp - src/math/lp/square_dense_submatrix.cpp - src/math/lp/row_eta_matrix.cpp - src/api/api_stats.cpp - src/api/api_special_relations.cpp - src/api/api_solver.cpp - src/api/api_seq.cpp - src/api/api_rcf.cpp - src/api/api_quant.cpp - src/api/api_qe.cpp - src/api/api_polynomial.cpp - src/api/api_pb.cpp - src/api/api_params.cpp - src/api/api_numeral.cpp - src/api/api_model.cpp - src/api/api_goal.cpp - src/api/api_fpa.cpp - src/api/api_datatype.cpp - src/api/api_context.cpp - src/api/api_config_params.cpp - src/api/api_bv.cpp - src/api/api_ast_vector.cpp - src/api/api_ast_map.cpp - src/api/api_ast.cpp - src/api/api_array.cpp - src/api/api_arith.cpp - src/api/api_algebraic.cpp - src/tactic/portfolio/solver_subsumption_tactic.cpp - src/tactic/portfolio/smt_strategic_solver.cpp - src/tactic/fpa/qffplra_tactic.cpp - src/tactic/ufbv/ufbv_rewriter_tactic.cpp - src/tactic/ufbv/quasi_macros_tactic.cpp - src/tactic/ufbv/macro_finder_tactic.cpp - src/muz/spacer/spacer_util.cpp - src/muz/spacer/spacer_prop_solver.cpp - src/muz/spacer/spacer_json.cpp - src/qe/qe_tactic.cpp - src/qe/qe_lite.cpp - src/qe/qe.cpp - src/tactic/sls/bvsls_opt_engine.cpp - src/smt/tactic/unit_subsumption_tactic.cpp - src/smt/tactic/smt_tactic_core.cpp - src/tactic/bv/max_bv_sharing_tactic.cpp - src/tactic/bv/elim_small_bv_tactic.cpp - src/tactic/bv/dt2bv_tactic.cpp - src/tactic/bv/bvarray2uf_tactic.cpp - src/tactic/bv/bv_size_reduction_tactic.cpp - src/tactic/bv/bv1_blaster_tactic.cpp - src/tactic/bv/bit_blaster_tactic.cpp - src/smt/user_propagator.cpp - src/smt/theory_wmaxsat.cpp - src/smt/theory_special_relations.cpp - src/smt/theory_pb.cpp - src/smt/theory_fpa.cpp - src/smt/theory_dummy.cpp - src/smt/theory_dl.cpp - src/smt/theory_char.cpp - src/smt/theory_bv.cpp - src/smt/theory_array_base.cpp - src/smt/theory_array.cpp - src/smt/smt_theory.cpp - src/smt/smt_relevancy.cpp - src/smt/smt_quick_checker.cpp - src/smt/smt_quantifier.cpp - src/smt/smt_model_generator.cpp - src/smt/smt_model_finder.cpp - src/smt/smt_model_checker.cpp - src/smt/smt_lookahead.cpp - src/smt/smt_kernel.cpp - src/smt/smt_justification.cpp - src/smt/smt_internalizer.cpp - src/smt/smt_for_each_relevant_expr.cpp - src/smt/smt_enode.cpp - src/smt/smt_context_stat.cpp - src/smt/smt_context_pp.cpp - src/smt/smt_context_inv.cpp - src/smt/smt_context.cpp - src/smt/smt_consequences.cpp - src/smt/smt_conflict_resolution.cpp - src/smt/smt_clause_proof.cpp - src/smt/smt_checker.cpp - src/smt/smt_case_split_queue.cpp - src/smt/smt_arith_value.cpp - src/smt/seq_offset_eq.cpp - src/smt/seq_axioms.cpp - src/smt/qi_queue.cpp - src/smt/mam.cpp - src/smt/expr_context_simplifier.cpp - src/smt/dyn_ack.cpp - src/smt/arith_eq_adapter.cpp - src/nlsat/tactic/nlsat_tactic.cpp - src/sat/tactic/sat_tactic.cpp - src/sat/smt/q_clause.cpp - src/sat/smt/pb_solver.cpp - src/sat/smt/pb_internalize.cpp - src/sat/smt/pb_card.cpp - src/sat/smt/fpa_solver.cpp - src/tactic/arith/recover_01_tactic.cpp - src/tactic/arith/pb2bv_tactic.cpp - src/tactic/arith/normalize_bounds_tactic.cpp - src/tactic/arith/nla2bv_tactic.cpp - src/tactic/arith/lia2pb_tactic.cpp - src/tactic/arith/lia2card_tactic.cpp - src/tactic/arith/fix_dl_var_tactic.cpp - src/tactic/arith/factor_tactic.cpp - src/tactic/arith/eq2bv_tactic.cpp - src/tactic/arith/diff_neq_tactic.cpp - src/tactic/arith/card2bv_tactic.cpp - src/tactic/arith/add_bounds_tactic.cpp - src/tactic/core/symmetry_reduce_tactic.cpp - src/tactic/core/split_clause_tactic.cpp - src/tactic/core/solve_eqs_tactic.cpp - src/tactic/core/reduce_args_tactic.cpp - src/tactic/core/propagate_values_tactic.cpp - src/tactic/core/pb_preprocess_tactic.cpp - src/tactic/core/occf_tactic.cpp - src/tactic/core/nnf_tactic.cpp - src/tactic/core/injectivity_tactic.cpp - src/tactic/core/elim_uncnstr_tactic.cpp - src/tactic/core/elim_term_ite_tactic.cpp - src/tactic/core/distribute_forall_tactic.cpp - src/tactic/core/der_tactic.cpp - src/tactic/core/collect_statistics_tactic.cpp - src/tactic/core/cofactor_term_ite_tactic.cpp - src/tactic/core/blast_term_ite_tactic.cpp - src/ackermannization/ackr_bound_probe.cpp - src/tactic/aig/aig_tactic.cpp - src/parsers/smt2/smt2scanner.cpp - src/parsers/smt2/smt2parser.cpp - src/cmd_context/tactic_cmds.cpp - src/solver/parallel_tactic.cpp - src/tactic/tactical.cpp - src/math/lp/lu.cpp - src/api/api_tactic.cpp - src/tactic/portfolio/default_tactic.cpp - src/opt/opt_lns.cpp - src/tactic/fpa/qffp_tactic.cpp - src/tactic/fpa/fpa2bv_tactic.cpp - src/tactic/ufbv/ufbv_tactic.cpp - src/tactic/smtlogics/quant_tactics.cpp - src/tactic/smtlogics/qfufbv_tactic.cpp - src/tactic/smtlogics/qfuf_tactic.cpp - src/tactic/smtlogics/qfnra_tactic.cpp - src/tactic/smtlogics/qfnia_tactic.cpp - src/tactic/smtlogics/qflra_tactic.cpp - src/tactic/smtlogics/qflia_tactic.cpp - src/tactic/smtlogics/qfidl_tactic.cpp - src/tactic/smtlogics/qfbv_tactic.cpp - src/tactic/smtlogics/qfauflia_tactic.cpp - src/tactic/smtlogics/qfaufbv_tactic.cpp - src/tactic/smtlogics/nra_tactic.cpp - src/muz/spacer/spacer_callback.cpp - src/sat/sat_solver/inc_sat_solver.cpp - src/tactic/sls/sls_tactic.cpp - src/smt/tactic/ctx_solver_simplify_tactic.cpp - src/tactic/bv/bv_bounds_tactic.cpp - src/tactic/bv/bv_bound_chk_tactic.cpp - src/smt/theory_utvpi.cpp - src/smt/theory_recfun.cpp - src/smt/theory_diff_logic.cpp - src/smt/theory_datatype.cpp - src/smt/theory_array_full.cpp - src/smt/theory_array_bapa.cpp - src/smt/smt_setup.cpp - src/smt/smt_parallel.cpp - src/smt/seq_regex.cpp - src/smt/seq_ne_solver.cpp - src/smt/seq_eq_solver.cpp - src/math/subpaving/tactic/subpaving_tactic.cpp - src/nlsat/tactic/qfnra_nlsat_tactic.cpp - src/sat/tactic/sat2goal.cpp - src/sat/tactic/goal2sat.cpp - src/tactic/arith/purify_arith_tactic.cpp - src/tactic/arith/propagate_ineqs_tactic.cpp - src/tactic/arith/fm_tactic.cpp - src/tactic/arith/degree_shift_tactic.cpp - src/tactic/core/tseitin_cnf_tactic.cpp - src/tactic/core/special_relations_tactic.cpp - src/tactic/core/simplify_tactic.cpp - src/tactic/core/dom_simplify_tactic.cpp - src/ackermannization/ackermannize_bv_tactic.cpp - src/tactic/core/ctx_simplify_tactic.cpp - src/math/lp/lp_core_solver_base.cpp - src/math/lp/core_solver_pretty_printer.cpp - src/api/dll/install_tactic.cpp - src/shell/install_tactic.cpp - src/opt/wmax.cpp - src/opt/sortmax.cpp - src/opt/optsmt.cpp - src/opt/opt_solver.cpp - src/opt/opt_parse.cpp - src/opt/opt_context.cpp - src/opt/maxsmt.cpp - src/opt/maxres.cpp - src/opt/maxlex.cpp - src/muz/ddnf/ddnf.cpp - src/muz/clp/clp_context.cpp - src/muz/spacer/spacer_sat_answer.cpp - src/muz/spacer/spacer_quant_generalizer.cpp - src/muz/spacer/spacer_pdr.cpp - src/muz/spacer/spacer_generalizers.cpp - src/muz/spacer/spacer_arith_generalizers.cpp - src/muz/transforms/dl_mk_separate_negated_tails.cpp - src/muz/transforms/dl_mk_unbound_compressor.cpp - src/muz/transforms/dl_mk_scale.cpp - src/muz/transforms/dl_mk_quantifier_instantiation.cpp - src/muz/transforms/dl_mk_quantifier_abstraction.cpp - src/muz/transforms/dl_mk_magic_symbolic.cpp - src/muz/transforms/dl_mk_magic_sets.cpp - src/muz/transforms/dl_mk_loop_counter.cpp - src/muz/transforms/dl_mk_karr_invariants.cpp - src/muz/transforms/dl_mk_filter_rules.cpp - src/muz/transforms/dl_mk_elim_term_ite.cpp - src/muz/transforms/dl_mk_coi_filter.cpp - src/muz/transforms/dl_mk_bit_blast.cpp - src/muz/transforms/dl_mk_backwards.cpp - src/muz/transforms/dl_mk_array_instantiation.cpp - src/muz/transforms/dl_mk_array_eq_rewrite.cpp - src/muz/transforms/dl_mk_array_blast.cpp - src/muz/dataflow/dataflow.cpp - src/muz/base/rule_properties.cpp - src/muz/base/dl_util.cpp - src/muz/base/dl_rule_transformer.cpp - src/muz/base/dl_rule_subsumption_index.cpp - src/muz/base/dl_rule_set.cpp - src/muz/base/dl_rule.cpp - src/muz/base/dl_costs.cpp - src/muz/base/dl_context.cpp - src/smt/theory_str_regex.cpp - src/smt/theory_str_mc.cpp - src/smt/theory_str.cpp - src/smt/theory_seq.cpp - src/smt/theory_dense_diff_logic.cpp - src/smt/theory_arith.cpp - src/sat/smt/q_queue.cpp - src/sat/smt/q_mam.cpp - src/sat/smt/q_eval.cpp - src/sat/smt/q_ematch.cpp - src/math/lp/lp_dual_core_solver.cpp - src/shell/opt_frontend.cpp - src/api/api_parsers.cpp - src/api/api_opt.cpp - src/opt/opt_cmds.cpp - src/muz/fp/horn_tactic.cpp - src/muz/fp/datalog_parser.cpp - src/muz/spacer/spacer_context.cpp - src/muz/rel/dl_external_relation.cpp - src/muz/transforms/dl_transforms.cpp - src/muz/transforms/dl_mk_unfold.cpp - src/muz/transforms/dl_mk_subsumption_checker.cpp - src/muz/transforms/dl_mk_slice.cpp - src/muz/transforms/dl_mk_rule_inliner.cpp - src/muz/transforms/dl_mk_interp_tail_simplifier.cpp - src/muz/transforms/dl_mk_coalesce.cpp - src/sat/smt/q_solver.cpp - src/sat/smt/q_model_fixer.cpp - src/sat/smt/q_mbi.cpp - src/math/lp/lp_solver.cpp - src/shell/smtlib_frontend.cpp - src/muz/bmc/dl_bmc_engine.cpp - src/muz/tab/tab_context.cpp - src/muz/spacer/spacer_legacy_frames.cpp - src/muz/spacer/spacer_dl_interface.cpp - src/muz/rel/udoc_relation.cpp - src/muz/rel/dl_table_relation.cpp - src/muz/rel/dl_table.cpp - src/muz/rel/dl_sparse_table.cpp - src/muz/rel/dl_mk_simple_joins.cpp - src/muz/rel/dl_mk_similarity_compressor.cpp - src/muz/rel/dl_lazy_table.cpp - src/muz/rel/dl_interval_relation.cpp - src/muz/rel/dl_check_table.cpp - src/muz/rel/dl_base.cpp - src/muz/rel/check_relation.cpp - src/muz/transforms/dl_mk_synchronize.cpp - src/math/lp/static_matrix.cpp - src/math/lp/mon_eq.cpp - src/math/lp/lp_primal_core_solver.cpp - src/math/lp/lp_dual_simplex.cpp - src/math/lp/lar_solver.cpp - src/math/lp/lar_core_solver.cpp - src/math/lp/int_gcd_test.cpp - src/math/lp/int_cube.cpp - src/math/lp/int_branch.cpp - src/math/lp/hnf_cutter.cpp - src/math/lp/gomory.cpp - src/muz/fp/dl_cmds.cpp - src/muz/rel/karr_relation.cpp - src/muz/rel/dl_sieve_relation.cpp - src/muz/rel/dl_relation_manager.cpp - src/muz/rel/dl_product_relation.cpp - src/muz/rel/dl_mk_explanations.cpp - src/muz/rel/dl_instruction.cpp - src/muz/rel/dl_finite_product_relation.cpp - src/muz/rel/dl_compiler.cpp - src/muz/rel/dl_bound_relation.cpp - src/muz/rel/aig_exporter.cpp - src/math/lp/random_updater.cpp - src/math/lp/lp_primal_simplex.cpp - src/math/lp/int_solver.cpp - src/math/lp/factorization.cpp - src/shell/lp_frontend.cpp - src/shell/datalog_frontend.cpp - src/api/api_datalog.cpp - src/muz/fp/dl_register_engine.cpp - src/muz/rel/rel_context.cpp - src/math/lp/nra_solver.cpp - src/math/lp/nla_tangent_lemmas.cpp - src/math/lp/nla_solver.cpp - src/math/lp/nla_order_lemmas.cpp - src/math/lp/nla_monotone_lemmas.cpp - src/math/lp/nla_intervals.cpp - src/math/lp/nla_core.cpp - src/math/lp/nla_common.cpp - src/math/lp/nla_basics_lemmas.cpp - src/math/lp/monomial_bounds.cpp - src/math/lp/horner.cpp - src/math/lp/factorization_factory_imp.cpp - src/math/lp/emonics.cpp - src/smt/theory_lra.cpp - src/sat/smt/euf_solver.cpp - src/sat/smt/arith_solver.cpp - src/sat/smt/arith_internalize.cpp - src/sat/smt/arith_diagnostics.cpp - src/sat/smt/arith_axioms.cpp - g++ -o z3 shell/gparams_register_modules.o shell/mem_initializer.o shell/install_tactic.o shell/z3_log_frontend.o shell/smtlib_frontend.o shell/opt_frontend.o shell/main.o shell/lp_frontend.o shell/drat_frontend.o shell/dimacs_frontend.o shell/datalog_frontend.o cmd_context/extra_cmds/extra_cmds.a api/api.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a sat/tactic/sat_tactic.a sat/smt/sat_smt.a qe/mbp/mbp.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/rewriter/bit_blaster/bit_blaster.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a solver/assertions/solver_assertions.a ast/pattern/pattern.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a solver/solver.a ast/proofs/proofs.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a math/lp/lp.a nlsat/nlsat.a sat/sat.a math/grobner/grobner.a smt/params/smt_params.a params/params.a ast/euf/euf.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/automata/automata.a math/hilbert/hilbert.a math/simplex/simplex.a math/dd/dd.a math/interval/interval.a math/polynomial/polynomial.a util/util.a -lpthread - g++ -o libz3.so -shared api/dll/gparams_register_modules.o api/dll/mem_initializer.o api/dll/install_tactic.o api/dll/dll.o api/api_commands.o api/api_log_macros.o api/z3_replayer.o api/api_tactic.o api/api_stats.o api/api_special_relations.o api/api_solver.o api/api_seq.o api/api_rcf.o api/api_quant.o api/api_qe.o api/api_polynomial.o api/api_pb.o api/api_parsers.o api/api_params.o api/api_opt.o api/api_numeral.o api/api_model.o api/api_log.o api/api_goal.o api/api_fpa.o api/api_datatype.o api/api_datalog.o api/api_context.o api/api_config_params.o api/api_bv.o api/api_ast_vector.o api/api_ast_map.o api/api_ast.o api/api_array.o api/api_arith.o api/api_algebraic.o cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a sat/tactic/sat_tactic.a sat/smt/sat_smt.a qe/mbp/mbp.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/rewriter/bit_blaster/bit_blaster.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a solver/assertions/solver_assertions.a ast/pattern/pattern.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a solver/solver.a ast/proofs/proofs.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a math/lp/lp.a nlsat/nlsat.a sat/sat.a math/grobner/grobner.a smt/params/smt_params.a params/params.a ast/euf/euf.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/automata/automata.a math/hilbert/hilbert.a math/simplex/simplex.a math/dd/dd.a math/interval/interval.a math/polynomial/polynomial.a util/util.a -lpthread -Wl,-soname,libz3.so - ln -f -s ../libz3.so python - ocamlfind ocamlc -package zarith -ccopt "-D_MP_INTERNAL -DNDEBUG -D_EXTERNAL_RELEASE -D_USE_THREAD_LOCAL -fvisibility=hidden -fvisibility-inlines-hidden -c -mfpmath=sse -msse -msse2 -O3 -D_LINUX_ -fPIC -I /home/opam/.opam/4.14/lib/ocaml -I ../src/api -I ../src/api/ml -o api/ml/z3native_stubs.o" -c ../src/api/ml/z3native_stubs.c - cc1: warning: command-line option '-fvisibility-inlines-hidden' is valid for C++/ObjC++ but not for C - ocamlmklib -o api/ml/z3ml -I api/ml -L. api/ml/z3native_stubs.o api/ml/z3enums.cmo api/ml/z3native.cmo api/ml/z3.cmo -lz3 -lstdc++ -ccopt -L$(ocamlfind printconf path)/stublibs -dllpath $(ocamlfind printconf path)/stublibs - ocamlmklib -o api/ml/z3ml -I api/ml -L. api/ml/z3native_stubs.o api/ml/z3enums.cmx api/ml/z3native.cmx api/ml/z3.cmx -lz3 -lstdc++ -ccopt -L$(ocamlfind printconf path)/stublibs -dllpath $(ocamlfind printconf path)/stublibs - ocamlfind ocamlopt -package zarith -linkall -shared -o api/ml/z3ml.cmxs -I . -I api/ml api/ml/z3ml.cmxa - Z3 was successfully built. - Z3Py scripts can already be executed in the 'build/python' directory. - Z3Py scripts stored in arbitrary directories can be executed if the 'build/python' directory is added to the PYTHONPATH environment variable and the 'build' directory is added to the LD_LIBRARY_PATH environment variable. - Use the following command to install Z3 at prefix /usr. - sudo make install - make: Leaving directory '/home/opam/.opam/4.14/.opam-switch/build/z3.4.8.13/build' -> compiled z3.4.8.13 Processing 19/21: [z3: sh] + /usr/bin/sh "-c" "ocamlfind install z3 build/api/ml/* -dll build/libz3.*" (CWD=/home/opam/.opam/4.14/.opam-switch/build/z3.4.8.13) - Installed /home/opam/.opam/4.14/lib/z3/z3native_stubs.o - Installed /home/opam/.opam/4.14/lib/z3/z3native.o - Installed /home/opam/.opam/4.14/lib/z3/z3native.mli - Installed /home/opam/.opam/4.14/lib/z3/z3native.cmx - Installed /home/opam/.opam/4.14/lib/z3/z3native.cmo - Installed /home/opam/.opam/4.14/lib/z3/z3native.cmi - Installed /home/opam/.opam/4.14/lib/z3/z3ml.cmxs - Installed /home/opam/.opam/4.14/lib/z3/z3ml.cmxa - Installed /home/opam/.opam/4.14/lib/z3/z3ml.cma - Installed /home/opam/.opam/4.14/lib/z3/z3ml.a - Installed /home/opam/.opam/4.14/lib/z3/z3enums.o - Installed /home/opam/.opam/4.14/lib/z3/z3enums.mli - Installed /home/opam/.opam/4.14/lib/z3/z3enums.cmx - Installed /home/opam/.opam/4.14/lib/z3/z3enums.cmo - Installed /home/opam/.opam/4.14/lib/z3/z3enums.cmi - Installed /home/opam/.opam/4.14/lib/z3/z3.o - Installed /home/opam/.opam/4.14/lib/z3/z3.mli - Installed /home/opam/.opam/4.14/lib/z3/z3.cmx - Installed /home/opam/.opam/4.14/lib/z3/z3.cmo - Installed /home/opam/.opam/4.14/lib/z3/z3.cmi - Installed /home/opam/.opam/4.14/lib/z3/libz3ml.a - Installed /home/opam/.opam/4.14/lib/stublibs/dllz3ml.so - Installed /home/opam/.opam/4.14/lib/stublibs/dllz3ml.so.owner - Installed /home/opam/.opam/4.14/lib/stublibs/libz3.so - Installed /home/opam/.opam/4.14/lib/stublibs/libz3.so.owner - ocamlfind: [WARNING] You have installed DLLs but the directory /home/opam/.opam/4.14/lib/stublibs is not mentioned in ld.conf - Installed /home/opam/.opam/4.14/lib/z3/META Processing 19/21: [z3: cp] + /usr/bin/cp "build/z3" "/home/opam/.opam/4.14/bin/z3" (CWD=/home/opam/.opam/4.14/.opam-switch/build/z3.4.8.13) -> installed z3.4.8.13 Processing 20/21: [z3_tptp: g++ z3_tptp] + /usr/bin/g++ "-I./src/api/c++" "-I./src/api" "-std=c++11" "-L/home/opam/.opam/4.14/lib/stublibs" "-o" "z3_tptp" "examples/tptp/tptp5.cpp" "examples/tptp/tptp5.lex.cpp" "-lz3" "-Wl,-rpath" "-Wl,/home/opam/.opam/4.14/lib/stublibs" (CWD=/home/opam/.opam/4.14/.opam-switch/build/z3_tptp.4.8.13) -> compiled z3_tptp.4.8.13 Processing 21/21: [z3_tptp: cp z3_tptp] + /usr/bin/cp "z3_tptp" "/home/opam/.opam/4.14/bin/z3_tptp" (CWD=/home/opam/.opam/4.14/.opam-switch/build/z3_tptp.4.8.13) -> installed z3_tptp.4.8.13 Done. <><> z3.4.8.13 installed successfully <><><><><><><><><><><><><><><><><><><><><> => This version of Z3 changed the linking mode from static to dynamic. This change is silent and potentially breaking. Please make sure that you don't require static binaries in the programs using Z3. # Run eval $(opam env) to update the current shell environment 2024-01-29 19:14.07 ---> saved as "4df7e6ae19d8c88185e01566dcd1927cc410e8cd2ecc190d9d118e7bc44c3296" /home/opam: (run (shell "opam exec -- ~/voodoo-prep -u z3_tptp:15dc5bf36fc07dfa3057fae176151995,z3:a5ca7c6c94219d0fa101939a04164a9e")) 2024-01-29 19:14.08 ---> saved as "61224d2b7549479ac2ff5f62a6f492d980046e5dc17aa1010beaf1ec3b85a301" /home/opam: (run (network host) (secrets (ssh_privkey (target /home/opam/.ssh/id_rsa)) (ssh_pubkey (target /home/opam/.ssh/id_rsa.pub)) (ssh_config (target /home/opam/.ssh/config))) (shell "(echo '0.501061') && (for DATA in prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13,z3.4.8.13-a5ca7c6c94219d0fa101939a04164a9e,z3.4.8.13 prep/universes/15dc5bf36fc07dfa3057fae176151995/z3_tptp/4.8.13,z3_tptp.4.8.13-15dc5bf36fc07dfa3057fae176151995,z3_tptp.4.8.13; do IFS=\",\"; set -- $DATA; ([ -d $1 ] || (echo \"FAILED:$2\" && mkdir -p $1 && cp ~/opam.err.log $1 && opam show $3 --raw > $1/opam)) && (shopt -s nullglob && ((tar -cvf $1.tar $1/* && rm -R $1/* && mv $1.tar $1/content.tar) || (echo 'Empty directory'))) done) && (for DATA in prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13,z3.4.8.13-a5ca7c6c94219d0fa101939a04164a9e,z3.4.8.13 prep/universes/15dc5bf36fc07dfa3057fae176151995/z3_tptp/4.8.13,z3_tptp.4.8.13-15dc5bf36fc07dfa3057fae176151995,z3_tptp.4.8.13; do IFS=\",\"; set -- $DATA; rsync -aR --no-p ./$1 docs.ci.ocaml.org:/data/.; done) && (for DATA in prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13,z3.4.8.13-a5ca7c6c94219d0fa101939a04164a9e,z3.4.8.13 prep/universes/15dc5bf36fc07dfa3057fae176151995/z3_tptp/4.8.13,z3_tptp.4.8.13-15dc5bf36fc07dfa3057fae176151995,z3_tptp.4.8.13; do IFS=\",\"; set -- $DATA; HASH=$((sha256sum $1/content.tar | cut -d \" \" -f 1) || echo -n 'empty'); printf \"HASHES:$2:$HASH\\n\"; done)")) 0.501061 prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13/lib/ prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13/lib/z3/ prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13/lib/z3/z3ml.ocamlobjinfo prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13/lib/z3/META prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13/lib/z3/z3.cmi prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13/lib/z3/z3enums.cmi prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13/lib/z3/z3native.cmi prep/universes/a5ca7c6c94219d0fa101939a04164a9e/z3/4.8.13/opam prep/universes/15dc5bf36fc07dfa3057fae176151995/z3_tptp/4.8.13/opam Warning: Permanently added '[docs.ci.ocaml.org]:2222' (ED25519) to the list of known hosts. Warning: Permanently added '[docs.ci.ocaml.org]:2222' (ED25519) to the list of known hosts. HASHES:z3.4.8.13-a5ca7c6c94219d0fa101939a04164a9e:73e939977fd926a7695ee5c87d90aaf7026c809997ab2dd793e8b6b7d1de1319 HASHES:z3_tptp.4.8.13-15dc5bf36fc07dfa3057fae176151995:c8d3c83d7ebd867c8d434a7c669f8564c5e243e7d40371e29ef31da13c5d4dab 2024-01-29 19:14.09 ---> saved as "9f35cff3685d48f95bbe5bca5b80398329e52c8bedede368268d1309442d663a" Job succeeded 2024-01-29 19:19.53: z3_tptp.4.8.13-15dc5bf36fc07dfa3057fae176151995 -> c8d3c83d7ebd867c8d434a7c669f8564c5e243e7d40371e29ef31da13c5d4dab 2024-01-29 19:19.53: z3.4.8.13-a5ca7c6c94219d0fa101939a04164a9e -> 73e939977fd926a7695ee5c87d90aaf7026c809997ab2dd793e8b6b7d1de1319 2024-01-29 19:19.53: Job succeeded