SuccessConsole Output

Push event to branch master
03:11:50 Connecting to https://api.github.com using dwightguth/****** (GitHub Access Token)
Obtained Jenkinsfile from 5220d3d8b1c3712973936e0af1417aea47f31f50
Running in Durability level: MAX_SURVIVABILITY
[Pipeline] Start of Pipeline
[Pipeline] ansiColor
[Pipeline] {
[Pipeline] stage
[Pipeline] { (Pull Request)
Stage "Pull Request" skipped due to when conditional
[Pipeline] stage
[Pipeline] { (Set title)
Stage "Pull Request" skipped due to when conditional
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Build docker image)
Stage "Pull Request" skipped due to when conditional
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Compile)
Stage "Pull Request" skipped due to when conditional
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Re-compile w/ timeout)
Stage "Pull Request" skipped due to when conditional
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Test)
Stage "Pull Request" skipped due to when conditional
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Test clean target)
Stage "Pull Request" skipped due to when conditional
[Pipeline] }
[Pipeline] // stage
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Merged to master)
[Pipeline] node
Running on rvwork-2 in /home/jenkins-slave/workspace/c-semantics_master
[Pipeline] {
[Pipeline] checkout
using credential github
Wiping out workspace first.
Cloning the remote Git repository
Cloning with configured refspecs honoured and without tags
Cloning repository https://github.com/kframework/c-semantics.git
 > git init /home/jenkins-slave/workspace/c-semantics_master # timeout=10
Fetching upstream changes from https://github.com/kframework/c-semantics.git
 > git --version # timeout=10
using GIT_ASKPASS to set credentials GitHub Access Token
 > git fetch --no-tags --progress https://github.com/kframework/c-semantics.git +refs/heads/master:refs/remotes/origin/master
Fetching without tags
Checking out Revision 5220d3d8b1c3712973936e0af1417aea47f31f50 (master)
 > git config remote.origin.url https://github.com/kframework/c-semantics.git # timeout=10
 > git config --add remote.origin.fetch +refs/heads/master:refs/remotes/origin/master # timeout=10
 > git config remote.origin.url https://github.com/kframework/c-semantics.git # timeout=10
Fetching upstream changes from https://github.com/kframework/c-semantics.git
using GIT_ASKPASS to set credentials GitHub Access Token
 > git fetch --no-tags --progress https://github.com/kframework/c-semantics.git +refs/heads/master:refs/remotes/origin/master
 > git config core.sparsecheckout # timeout=10
 > git checkout -f 5220d3d8b1c3712973936e0af1417aea47f31f50
Commit message: "Fix nested switch (#605)"
 > git rev-list --no-walk ed5c05e4ac070e31cc45331e5b0752357fbeeea3 # timeout=10
 > git remote # timeout=10
 > git submodule init # timeout=10
 > git submodule sync # timeout=10
 > git config --get remote.origin.url # timeout=10
 > git submodule init # timeout=10
 > git config -f .gitmodules --get-regexp ^submodule\.(.+)\.url # timeout=10
 > git config --get submodule..build/k.url # timeout=10
 > git config -f .gitmodules --get submodule..build/k.path # timeout=10
 > git submodule update --init --recursive .build/k
[Pipeline] withEnv
[Pipeline] {
[Pipeline] stage
[Pipeline] { (Build docker image)
[Pipeline] script
[Pipeline] {
[Pipeline] sh
+ docker build -t runtimeverificationinc/c-semantics:latest .
Sending build context to Docker daemon  297.5MB

Step 1/10 : FROM runtimeverificationinc/kframework:ubuntu-bionic
ubuntu-bionic: Pulling from runtimeverificationinc/kframework
Digest: sha256:65502b8e0b47e416b7f51d7b37b07256c41829c5edc545e3ddfe3688c81d6218
Status: Downloaded newer image for runtimeverificationinc/kframework:ubuntu-bionic
 ---> 5a700dd2c3ad
Step 2/10 : RUN     apt-get update -q     &&  apt install --yes           libstdc++6                llvm-6.0                  clang++-6.0               clang-6.0
 ---> Running in 2943724eb87a
Get:1 http://security.ubuntu.com/ubuntu bionic-security InRelease [88.7 kB]
Hit:2 http://archive.ubuntu.com/ubuntu bionic InRelease
Get:3 http://archive.ubuntu.com/ubuntu bionic-updates InRelease [88.7 kB]
Get:4 http://archive.ubuntu.com/ubuntu bionic-backports InRelease [74.6 kB]
Get:5 http://security.ubuntu.com/ubuntu bionic-security/multiverse amd64 Packages [7064 B]
Get:6 http://archive.ubuntu.com/ubuntu bionic-updates/multiverse amd64 Packages [11.1 kB]
Get:7 http://security.ubuntu.com/ubuntu bionic-security/restricted amd64 Packages [27.5 kB]
Get:8 http://security.ubuntu.com/ubuntu bionic-security/universe amd64 Packages [818 kB]
Get:9 http://archive.ubuntu.com/ubuntu bionic-updates/restricted amd64 Packages [41.2 kB]
Get:10 http://archive.ubuntu.com/ubuntu bionic-updates/universe amd64 Packages [1345 kB]
Get:11 http://security.ubuntu.com/ubuntu bionic-security/main amd64 Packages [817 kB]
Get:12 http://archive.ubuntu.com/ubuntu bionic-updates/main amd64 Packages [1104 kB]
Get:13 http://archive.ubuntu.com/ubuntu bionic-backports/universe amd64 Packages [4252 B]
Fetched 4426 kB in 1s (3189 kB/s)
Reading package lists...

WARNING: apt does not have a stable CLI interface. Use with caution in scripts.

Reading package lists...
Building dependency tree...
Reading state information...
libstdc++6 is already the newest version (8.3.0-6ubuntu1~18.04.1).
The following additional packages will be installed:
  libclang-common-6.0-dev libclang1-6.0 libllvm6.0 libomp-8-dev libomp5-8
  llvm-6.0-dev llvm-6.0-runtime
Suggested packages:
  gnustep gnustep-devel libomp-8-doc llvm-6.0-doc
Recommended packages:
  libomp-dev
The following NEW packages will be installed:
  clang-6.0 clang-6.0-doc clang-6.0-examples libclang-6.0-dev
  libclang-common-6.0-dev libclang1-6.0 libllvm6.0 llvm-6.0 llvm-6.0-dev
  llvm-6.0-runtime python-clang-6.0
The following packages will be upgraded:
  libomp-8-dev libomp5-8
2 upgraded, 11 newly installed, 0 to remove and 90 not upgraded.
Need to get 83.7 MB of archives.
After this operation, 661 MB of additional disk space will be used.
Get:1 http://archive.ubuntu.com/ubuntu bionic/main amd64 libllvm6.0 amd64 1:6.0-1ubuntu2 [14.5 MB]
Get:2 http://archive.ubuntu.com/ubuntu bionic/universe amd64 libclang-common-6.0-dev amd64 1:6.0-1ubuntu2 [3078 kB]
Get:3 http://archive.ubuntu.com/ubuntu bionic/main amd64 libclang1-6.0 amd64 1:6.0-1ubuntu2 [7067 kB]
Get:4 http://archive.ubuntu.com/ubuntu bionic/universe amd64 clang-6.0 amd64 1:6.0-1ubuntu2 [9292 kB]
Get:5 http://archive.ubuntu.com/ubuntu bionic/universe amd64 clang-6.0-doc all 1:6.0-1ubuntu2 [911 kB]
Get:6 http://archive.ubuntu.com/ubuntu bionic/universe amd64 clang-6.0-examples amd64 1:6.0-1ubuntu2 [15.6 kB]
Get:7 http://archive.ubuntu.com/ubuntu bionic/universe amd64 libclang-6.0-dev amd64 1:6.0-1ubuntu2 [20.4 MB]
Get:8 http://archive.ubuntu.com/ubuntu bionic-updates/universe amd64 libomp-8-dev amd64 1:8-3~ubuntu18.04.2 [56.2 kB]
Get:9 http://archive.ubuntu.com/ubuntu bionic-updates/universe amd64 libomp5-8 amd64 1:8-3~ubuntu18.04.2 [299 kB]
Get:10 http://archive.ubuntu.com/ubuntu bionic/main amd64 llvm-6.0-runtime amd64 1:6.0-1ubuntu2 [200 kB]
Get:11 http://archive.ubuntu.com/ubuntu bionic/main amd64 llvm-6.0 amd64 1:6.0-1ubuntu2 [4838 kB]
Get:12 http://archive.ubuntu.com/ubuntu bionic/main amd64 llvm-6.0-dev amd64 1:6.0-1ubuntu2 [23.0 MB]
Get:13 http://archive.ubuntu.com/ubuntu bionic/universe amd64 python-clang-6.0 amd64 1:6.0-1ubuntu2 [32.9 kB]
debconf: delaying package configuration, since apt-utils is not installed
Fetched 83.7 MB in 4s (21.6 MB/s)
Selecting previously unselected package libllvm6.0: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 ... 51373 files and directories currently installed.)
Preparing to unpack .../00-libllvm6.0_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking libllvm6.0:amd64 (1:6.0-1ubuntu2) ...
Selecting previously unselected package libclang-common-6.0-dev.
Preparing to unpack .../01-libclang-common-6.0-dev_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking libclang-common-6.0-dev (1:6.0-1ubuntu2) ...
Selecting previously unselected package libclang1-6.0:amd64.
Preparing to unpack .../02-libclang1-6.0_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking libclang1-6.0:amd64 (1:6.0-1ubuntu2) ...
Selecting previously unselected package clang-6.0.
Preparing to unpack .../03-clang-6.0_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking clang-6.0 (1:6.0-1ubuntu2) ...
Selecting previously unselected package clang-6.0-doc.
Preparing to unpack .../04-clang-6.0-doc_1%3a6.0-1ubuntu2_all.deb ...
Unpacking clang-6.0-doc (1:6.0-1ubuntu2) ...
Selecting previously unselected package clang-6.0-examples.
Preparing to unpack .../05-clang-6.0-examples_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking clang-6.0-examples (1:6.0-1ubuntu2) ...
Selecting previously unselected package libclang-6.0-dev.
Preparing to unpack .../06-libclang-6.0-dev_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking libclang-6.0-dev (1:6.0-1ubuntu2) ...
Preparing to unpack .../07-libomp-8-dev_1%3a8-3~ubuntu18.04.2_amd64.deb ...
Unpacking libomp-8-dev (1:8-3~ubuntu18.04.2) over (1:8-3~ubuntu18.04.1) ...
Preparing to unpack .../08-libomp5-8_1%3a8-3~ubuntu18.04.2_amd64.deb ...
Unpacking libomp5-8:amd64 (1:8-3~ubuntu18.04.2) over (1:8-3~ubuntu18.04.1) ...
Selecting previously unselected package llvm-6.0-runtime.
Preparing to unpack .../09-llvm-6.0-runtime_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking llvm-6.0-runtime (1:6.0-1ubuntu2) ...
Selecting previously unselected package llvm-6.0.
Preparing to unpack .../10-llvm-6.0_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking llvm-6.0 (1:6.0-1ubuntu2) ...
Selecting previously unselected package llvm-6.0-dev.
Preparing to unpack .../11-llvm-6.0-dev_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking llvm-6.0-dev (1:6.0-1ubuntu2) ...
Selecting previously unselected package python-clang-6.0.
Preparing to unpack .../12-python-clang-6.0_1%3a6.0-1ubuntu2_amd64.deb ...
Unpacking python-clang-6.0 (1:6.0-1ubuntu2) ...
Setting up libllvm6.0:amd64 (1:6.0-1ubuntu2) ...
Setting up libomp5-8:amd64 (1:8-3~ubuntu18.04.2) ...
Setting up libclang1-6.0:amd64 (1:6.0-1ubuntu2) ...
Setting up llvm-6.0-runtime (1:6.0-1ubuntu2) ...
mount: /proc/sys/fs/binfmt_misc: permission denied.
update-binfmts: warning: Couldn't mount the binfmt_misc filesystem on /proc/sys/fs/binfmt_misc.
Setting up clang-6.0-examples (1:6.0-1ubuntu2) ...
Setting up libomp-8-dev (1:8-3~ubuntu18.04.2) ...
Processing triggers for libc-bin (2.27-3ubuntu1) ...
Setting up llvm-6.0 (1:6.0-1ubuntu2) ...
Processing triggers for man-db (2.8.3-2ubuntu0.1) ...
Setting up python-clang-6.0 (1:6.0-1ubuntu2) ...
Setting up clang-6.0-doc (1:6.0-1ubuntu2) ...
Setting up libclang-common-6.0-dev (1:6.0-1ubuntu2) ...
Setting up libclang-6.0-dev (1:6.0-1ubuntu2) ...
Setting up llvm-6.0-dev (1:6.0-1ubuntu2) ...
Setting up clang-6.0 (1:6.0-1ubuntu2) ...
Processing triggers for libc-bin (2.27-3ubuntu1) ...
Removing intermediate container 2943724eb87a
 ---> 1819d4040974
Step 3/10 : RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.7     && cd z3                                                            && python scripts/mk_make.py                                        && cd build                                                         && make -j8                                                         && make install                                                     && cd ../..                                                         && rm -rf z3
 ---> Running in 94512d2c6fd6
Cloning into 'z3'...
Note: checking out '30e7c225cd510400eacd41d0a83e013b835a8ece'.

You are in 'detached HEAD' state. You can look around, make experimental
changes and commit them, and you can discard any commits you make in this
state without impacting any branches by performing another checkout.

If you want to create a new branch to retain commits you create, you may
do so (now or later) by using -b with the checkout command again. Example:

  git checkout -b <new-branch-name>

New component: 'util'
New component: 'polynomial'
New component: 'sat'
New component: 'nlsat'
New component: 'lp'
New component: 'hilbert'
New component: 'simplex'
New component: 'automata'
New component: 'interval'
New component: 'realclosure'
New component: 'subpaving'
New component: 'ast'
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: 'grobner'
New component: 'euclid'
New component: 'proofs'
New component: 'solver'
New component: 'cmd_context'
New component: 'sat_tactic'
New component: 'smt2parser'
New component: 'pattern'
New component: 'core_tactics'
New component: 'arith_tactics'
New component: 'nlsat_tactic'
New component: 'subpaving_tactic'
New component: 'aig_tactic'
New component: 'ackermannization'
New component: 'fpa'
New component: 'bit_blaster'
New component: 'smt_params'
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: 'ufbv_tactic'
New component: 'smtlogic_tactics'
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/math/realclosure/rcf_params.hpp'
Generated 'src/math/polynomial/algebraic_params.hpp'
Generated 'src/model/model_evaluator_params.hpp'
Generated 'src/model/model_params.hpp'
Generated 'src/sat/sat_params.hpp'
Generated 'src/sat/sat_simplifier_params.hpp'
Generated 'src/sat/sat_scc_params.hpp'
Generated 'src/sat/sat_asymm_branch_params.hpp'
Generated 'src/nlsat/nlsat_params.hpp'
Generated 'src/opt/opt_params.hpp'
Generated 'src/tactic/tactic_params.hpp'
Generated 'src/tactic/sls/sls_params.hpp'
Generated 'src/tactic/smtlogics/qfufbv_tactic_params.hpp'
Generated 'src/solver/combined_solver_params.hpp'
Generated 'src/solver/parallel_params.hpp'
Generated 'src/solver/solver_params.hpp'
Generated 'src/muz/base/fp_params.hpp'
Generated 'src/ackermannization/ackermannization_params.hpp'
Generated 'src/ackermannization/ackermannize_bv_tactic_params.hpp'
Generated 'src/util/lp/lp_params.hpp'
Generated 'src/ast/pp_params.hpp'
Generated 'src/ast/rewriter/bv_rewriter_params.hpp'
Generated 'src/ast/rewriter/poly_rewriter_params.hpp'
Generated 'src/ast/rewriter/bool_rewriter_params.hpp'
Generated 'src/ast/rewriter/arith_rewriter_params.hpp'
Generated 'src/ast/rewriter/rewriter_params.hpp'
Generated 'src/ast/rewriter/fpa_rewriter_params.hpp'
Generated 'src/ast/rewriter/array_rewriter_params.hpp'
Generated 'src/ast/pattern/pattern_inference_params_helper.hpp'
Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp'
Generated 'src/ast/normal_forms/nnf_params.hpp'
Generated 'src/smt/params/smt_params_helper.hpp'
Generated 'src/parsers/util/parser_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 solver
Component tactic
Component proofs
Component sat_solver
Component core_tactics
Component macros
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 sat_tactic
Component nlsat_tactic
Component nlsat
Component smt_tactic
Component smt
Component proto_model
Component smt_params
Component substitution
Component grobner
Component euclid
Component simplex
Component fpa
Component lp
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 interval
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 solver
Component tactic
Component proofs
Component sat_solver
Component core_tactics
Component macros
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 sat_tactic
Component nlsat_tactic
Component nlsat
Component smt_tactic
Component smt
Component proto_model
Component smt_params
Component substitution
Component grobner
Component euclid
Component simplex
Component fpa
Component lp
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 interval
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 solver
Component tactic
Component proofs
Component sat_solver
Component core_tactics
Component macros
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 sat_tactic
Component nlsat_tactic
Component nlsat
Component smt_tactic
Component smt
Component proto_model
Component smt_params
Component substitution
Component grobner
Component euclid
Component simplex
Component fpa
Component lp
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 interval
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'
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 'z3.py'
Copied 'z3consts.py'
Copied 'z3core.py'
Copied 'z3types.py'
Copied 'z3num.py'
Copied 'z3poly.py'
Copied '__init__.py'
Copied 'z3util.py'
Copied 'z3printer.py'
Copied 'z3rcf.py'
Copied 'z3types.pyc'
Copied 'z3rcf.pyc'
Copied 'z3core.pyc'
Copied 'z3printer.pyc'
Copied 'z3poly.pyc'
Copied 'z3util.pyc'
Copied 'z3consts.pyc'
Copied 'z3num.pyc'
Copied 'z3.pyc'
Copied '__init__.pyc'
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/python2.7/dist-packages
Python version: 2.7
Writing build/Makefile
Copied Z3Py example 'rc2.py' to 'build/python'
Copied Z3Py example 'visitor.py' to 'build/python'
Copied Z3Py example 'trafficjam.py' to 'build/python'
Copied Z3Py example 'parallel.py' to 'build/python'
Copied Z3Py example 'all_interval_series.py' to 'build/python'
Copied Z3Py example 'mini_ic3.py' to 'build/python'
Copied Z3Py example 'union_sort.py' to 'build/python'
Copied Z3Py example 'example.py' to 'build/python'
Copied Z3Py example 'socrates.py' to 'build/python'
Copied Z3Py example 'mini_quip.py' to 'build/python'
Makefile was successfully generated.
  compilation mode: Release
Type 'cd build; make' to build Z3
src/smt/smt_statistics.cpp
src/util/common_msgs.cpp
src/util/luby.cpp
src/util/approx_nat.cpp
src/api/dll/dll.cpp
src/util/memory_manager.cpp
src/util/z3_exception.cpp
src/util/timeit.cpp
src/util/util.cpp
src/util/timeout.cpp
src/util/scoped_timer.cpp
src/util/page.cpp
src/util/stack.cpp
src/util/approx_set.cpp
src/util/bit_util.cpp
src/util/scoped_ctrl_c.cpp
src/shell/z3_log_frontend.cpp
src/api/api_commands.cpp
src/api/api_log.cpp
src/util/fixed_bit_vector.cpp
src/util/hash.cpp
src/util/lbool.cpp
src/solver/smt_logics.cpp
src/util/mpn.cpp
src/util/smt2_util.cpp
src/api/api_log_macros.cpp
src/util/cmd_context_types.cpp
src/util/permutation.cpp
src/util/min_cut.cpp
src/util/warning.cpp
src/util/small_object_allocator.cpp
src/ast/pattern/pattern_inference_params.cpp
src/sat/sat_config.cpp
src/util/bit_vector.cpp
src/util/prime_generator.cpp
src/util/debug.cpp
src/util/trace.cpp
src/util/rlimit.cpp
src/util/env_params.cpp
src/util/region.cpp
src/util/symbol.cpp
src/api/z3_replayer.cpp
src/smt/params/qi_params.cpp
src/smt/params/theory_array_params.cpp
src/smt/params/theory_pb_params.cpp
src/smt/params/theory_arith_params.cpp
src/smt/params/theory_str_params.cpp
src/smt/params/theory_seq_params.cpp
src/smt/params/theory_bv_params.cpp
src/smt/params/preprocessor_params.cpp
src/smt/params/dyn_ack_params.cpp
src/math/automata/automaton.cpp
src/sat/sat_watched.cpp
src/sat/sat_clause.cpp
src/sat/sat_clause_use_list.cpp
src/util/mpz.cpp
src/util/statistics.cpp
src/math/euclid/euclidean_solver.cpp
src/math/realclosure/mpz_matrix.cpp
src/math/interval/interval_mpq.cpp
src/sat/sat_bdd.cpp
src/sat/sat_clause_set.cpp
src/util/mpff.cpp
src/util/mpf.cpp
src/util/mpq.cpp
src/util/mpq_inf.cpp
src/util/hwf.cpp
src/util/gparams.cpp
src/util/mpfx.cpp
src/shell/mem_initializer.cpp
src/smt/old_interval.cpp
src/tactic/arith/linear_equation.cpp
src/math/subpaving/subpaving.cpp
src/math/subpaving/subpaving_mpf.cpp
src/math/subpaving/subpaving_hwf.cpp
src/math/realclosure/realclosure.cpp
src/util/params.cpp
src/util/mpbq.cpp
src/util/s_integer.cpp
src/util/rational.cpp
src/util/inf_int_rational.cpp
src/api/dll/mem_initializer.cpp
src/muz/spacer/spacer_matrix.cpp
src/muz/rel/tbv.cpp
src/muz/base/bind_variables.cpp
src/smt/smt_quantifier_stat.cpp
src/smt/params/smt_params.cpp
src/tactic/arith/bound_propagator.cpp
src/ast/rewriter/func_decl_replace.cpp
src/ast/used_vars.cpp
src/ast/has_free_vars.cpp
src/ast/display_dimacs.cpp
src/ast/act_cache.cpp
src/ast/num_occurs.cpp
src/ast/for_each_ast.cpp
src/ast/special_relations_decl_plugin.cpp
src/ast/ast_lt.cpp
src/ast/expr_map.cpp
src/math/subpaving/subpaving_mpq.cpp
src/math/subpaving/subpaving_mpff.cpp
src/math/subpaving/subpaving_mpfx.cpp
src/math/simplex/simplex.cpp
src/math/hilbert/hilbert_basis.cpp
src/util/lp/lp_utils.cpp
src/sat/sat_prob.cpp
src/sat/sat_probing.cpp
src/sat/sat_iff3_finder.cpp
src/sat/sat_ddfw.cpp
src/sat/sat_lookahead.cpp
src/sat/sat_drat.cpp
src/sat/sat_simplifier.cpp
src/sat/sat_model_converter.cpp
src/sat/sat_big.cpp
src/sat/sat_scc.cpp
src/sat/sat_elim_eqs.cpp
src/sat/dimacs.cpp
src/sat/sat_parallel.cpp
src/sat/sat_integrity_checker.cpp
src/sat/sat_cleaner.cpp
src/sat/sat_asymm_branch.cpp
src/sat/sat_elim_vars.cpp
src/sat/sat_mus.cpp
src/util/inf_rational.cpp
src/util/sexpr.cpp
src/util/inf_s_integer.cpp
src/api/dll/gparams_register_modules.cpp
src/shell/gparams_register_modules.cpp
src/smt/uses_theory.cpp
src/smt/arith_eq_solver.cpp
src/smt/smt_value_sort.cpp
src/ackermannization/ackr_helper.cpp
src/math/subpaving/tactic/expr2subpaving.cpp
src/parsers/util/scanner.cpp
src/parsers/util/simple_parser.cpp
src/parsers/util/cost_parser.cpp
src/model/value_factory.cpp
src/ast/rewriter/mk_extract_proc.cpp
src/ast/rewriter/ast_counter.cpp
src/ast/rewriter/distribute_forall.cpp
src/ast/rewriter/datatype_rewriter.cpp
src/ast/rewriter/dl_rewriter.cpp
src/ast/ast_util.cpp
src/ast/format.cpp
src/ast/expr_functors.cpp
src/ast/func_decl_dependencies.cpp
src/ast/csp_decl_plugin.cpp
src/ast/reg_decl_plugins.cpp
src/ast/for_each_expr.cpp
src/ast/ast_ll_pp.cpp
src/ast/occurs.cpp
src/ast/pp.cpp
src/ast/expr_stat.cpp
src/ast/macro_substitution.cpp
src/sat/sat_unit_walk.cpp
src/sat/sat_solver.cpp
src/math/polynomial/polynomial_cache.cpp
src/shell/main.cpp
src/qe/qe_solve_plugin.cpp
src/smt/fingerprints.cpp
src/smt/cost_evaluator.cpp
src/smt/elim_term_ite.cpp
src/smt/cached_var_subst.cpp
src/smt/smt_literal.cpp
src/smt/smt_farkas_util.cpp
src/ast/fpa/fpa2bv_converter.cpp
src/ast/fpa/fpa2bv_rewriter.cpp
src/tactic/arith/bv2real_rewriter.cpp
src/ast/pattern/pattern_inference.cpp
src/cmd_context/tactic_manager.cpp
src/cmd_context/check_logic.cpp
src/cmd_context/pdecl.cpp
src/ast/proofs/proof_utils.cpp
src/ast/proofs/proof_checker.cpp
src/math/grobner/grobner.cpp
src/parsers/util/pattern_validation.cpp
src/tactic/equiv_proof_converter.cpp
src/tactic/replace_proof_converter.cpp
src/model/numeral_factory.cpp
src/model/func_interp.cpp
src/ast/normal_forms/pull_quant.cpp
src/ast/normal_forms/nnf.cpp
src/ast/normal_forms/name_exprs.cpp
src/ast/normal_forms/defined_names.cpp
src/ast/rewriter/bool_rewriter.cpp
src/ast/rewriter/maximize_ac_sharing.cpp
src/ast/rewriter/var_subst.cpp
src/ast/rewriter/enum2bv_rewriter.cpp
src/ast/rewriter/bv_trailing.cpp
src/ast/rewriter/arith_rewriter.cpp
src/ast/rewriter/array_rewriter.cpp
src/ast/rewriter/rewriter.cpp
src/ast/rewriter/push_app_ite.cpp
src/ast/rewriter/expr_safe_replace.cpp
src/ast/rewriter/pb_rewriter.cpp
src/ast/rewriter/quant_hoist.cpp
src/ast/rewriter/hoist_rewriter.cpp
src/ast/rewriter/pb2bv_rewriter.cpp
src/ast/rewriter/elim_bounds.cpp
src/ast/rewriter/fpa_rewriter.cpp
src/ast/rewriter/bv_elim.cpp
src/ast/rewriter/label_rewriter.cpp
src/ast/rewriter/bv_bounds.cpp
src/ast/rewriter/expr_replacer.cpp
src/ast/rewriter/factor_rewriter.cpp
src/ast/rewriter/seq_rewriter.cpp
src/ast/rewriter/factor_equivs.cpp
src/ast/rewriter/inj_axiom.cpp
src/ast/rewriter/der.cpp
src/ast/ast.cpp
src/ast/arith_decl_plugin.cpp
src/ast/ast_smt2_pp.cpp
src/ast/well_sorted.cpp
src/ast/fpa_decl_plugin.cpp
src/ast/expr2var.cpp
src/ast/expr_abstract.cpp
src/ast/array_decl_plugin.cpp
src/ast/ast_translation.cpp
src/ast/decl_collector.cpp
src/ast/dl_decl_plugin.cpp
src/ast/seq_decl_plugin.cpp
src/ast/ast_pp_dot.cpp
src/ast/expr2polynomial.cpp
src/ast/recfun_decl_plugin.cpp
src/ast/datatype_decl_plugin.cpp
src/ast/expr_substitution.cpp
src/ast/static_features.cpp
src/ast/shared_occs.cpp
src/ast/ast_smt_pp.cpp
src/ast/pb_decl_plugin.cpp
src/ast/bv_decl_plugin.cpp
src/math/simplex/model_based_opt.cpp
src/util/lp/lp_settings.cpp
src/util/lp/binary_heap_priority_queue.cpp
src/nlsat/nlsat_types.cpp
src/nlsat/nlsat_clause.cpp
src/nlsat/nlsat_interval_set.cpp
src/sat/ba_solver.cpp
src/sat/sat_local_search.cpp
src/math/polynomial/rpolynomial.cpp
src/math/polynomial/algebraic_numbers.cpp
src/math/polynomial/upolynomial.cpp
src/math/polynomial/polynomial.cpp
src/muz/spacer/spacer_antiunify.cpp
src/smt/smt_clause.cpp
src/smt/smt_almost_cg_table.cpp
src/smt/theory_opt.cpp
src/smt/watch_list.cpp
src/smt/smt_cg_table.cpp
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
src/ast/rewriter/bit_blaster/bit_blaster.cpp
src/ast/fpa/bv2fpa_converter.cpp
src/ast/substitution/substitution_tree.cpp
src/ast/substitution/matcher.cpp
src/ast/substitution/substitution.cpp
src/ast/substitution/unifier.cpp
src/model/struct_factory.cpp
src/model/array_factory.cpp
src/model/datatype_factory.cpp
src/model/model_pp.cpp
src/model/model_v2_pp.cpp
src/model/model_smt2_pp.cpp
src/model/model_core.cpp
src/ast/rewriter/bv_rewriter.cpp
src/ast/rewriter/mk_simplified_app.cpp
src/ast/rewriter/th_rewriter.cpp
src/ast/ast_pp_util.cpp
src/ast/ast_printer.cpp
src/util/lp/indexed_vector.cpp
src/util/lp/binary_heap_upair_queue.cpp
src/util/lp/dense_matrix.cpp
src/math/polynomial/sexpr2upolynomial.cpp
src/tactic/ufbv/ufbv_rewriter.cpp
src/muz/spacer/spacer_mev_array.cpp
src/muz/spacer/spacer_sem_matcher.cpp
src/muz/spacer/spacer_iuc_proof.cpp
src/muz/spacer/spacer_sym_mux.cpp
src/qe/qe_array_plugin.cpp
src/qe/qe_term_graph.cpp
src/qe/nlarith_util.cpp
src/qe/qe_bv_plugin.cpp
src/qe/qe_bool_plugin.cpp
src/qe/qe_dl_plugin.cpp
src/qe/qe_datatype_plugin.cpp
src/smt/proto_model/proto_model.cpp
src/model/model2expr.cpp
src/model/model_implicant.cpp
src/model/model.cpp
src/model/model_evaluator.cpp
src/ast/macros/macro_util.cpp
src/ast/rewriter/bit2int.cpp
src/nlsat/nlsat_solver.cpp
src/nlsat/nlsat_evaluator.cpp
src/nlsat/nlsat_explain.cpp
src/math/polynomial/upolynomial_factorization.cpp
src/opt/pb_sls.cpp
src/muz/spacer/spacer_mbc.cpp
src/muz/spacer/spacer_unsat_core_learner.cpp
src/muz/spacer/spacer_qe_project.cpp
src/muz/rel/doc.cpp
src/muz/base/dl_boogie_proof.cpp
src/qe/qe_arith.cpp
src/qe/qe_datatypes.cpp
src/qe/qe_arith_plugin.cpp
src/tactic/bv/bit_blaster_model_converter.cpp
src/smt/expr_context_simplifier.cpp
src/ackermannization/ackermannize_bv_model_converter.cpp
src/ackermannization/lackr_model_constructor.cpp
src/ackermannization/ackr_model_converter.cpp
src/tactic/model_converter.cpp
src/tactic/horn_subsume_model_converter.cpp
src/ast/macros/macro_manager.cpp
src/ast/macros/quasi_macros.cpp
src/util/lp/matrix.cpp
src/util/lp/permutation_matrix.cpp
src/tactic/fpa/fpa2bv_model_converter.cpp
src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp
src/muz/spacer/spacer_proof_utils.cpp
src/muz/spacer/spacer_farkas_learner.cpp
src/muz/base/hnf.cpp
src/qe/qe_arrays.cpp
src/qe/qe_mbp.cpp
src/ackermannization/lackr_model_converter_lazy.cpp
src/tactic/aig/aig.cpp
src/tactic/arith/bound_manager.cpp
src/tactic/arith/pb2bv_model_converter.cpp
src/tactic/arith/bv2int_rewriter.cpp
src/tactic/arith/probe_arith.cpp
src/tactic/core/collect_occs.cpp
src/sat/tactic/atom2bool_var.cpp
src/solver/check_sat_result.cpp
src/tactic/dependency_converter.cpp
src/tactic/probe.cpp
src/tactic/goal.cpp
src/tactic/proof_converter.cpp
src/tactic/goal_num_occurs.cpp
src/tactic/goal_util.cpp
src/tactic/generic_model_converter.cpp
src/tactic/goal_shared_occs.cpp
src/ast/macros/macro_finder.cpp
src/util/lp/scaler.cpp
src/util/lp/eta_matrix.cpp
src/shell/dimacs_frontend.cpp
src/opt/opt_pareto.cpp
src/tactic/portfolio/solver2lookahead.cpp
src/tactic/portfolio/default_tactic.cpp
src/tactic/fpa/fpa2bv_tactic.cpp
src/tactic/fpa/qffplra_tactic.cpp
src/tactic/smtlogics/qfnia_tactic.cpp
src/tactic/smtlogics/qfuf_tactic.cpp
src/tactic/smtlogics/qflra_tactic.cpp
src/tactic/smtlogics/qfidl_tactic.cpp
src/tactic/smtlogics/qfauflia_tactic.cpp
src/tactic/smtlogics/qfnra_tactic.cpp
src/tactic/smtlogics/qflia_tactic.cpp
src/tactic/smtlogics/nra_tactic.cpp
src/tactic/ufbv/ufbv_tactic.cpp
src/tactic/ufbv/quasi_macros_tactic.cpp
src/tactic/ufbv/macro_finder_tactic.cpp
src/tactic/ufbv/ufbv_rewriter_tactic.cpp
src/muz/spacer/spacer_unsat_core_plugin.cpp
src/muz/spacer/spacer_iuc_solver.cpp
src/tactic/fd_solver/smtfd_solver.cpp
src/tactic/fd_solver/pb2bv_solver.cpp
src/tactic/fd_solver/bounded_int2bv_solver.cpp
src/tactic/fd_solver/enum2bv_solver.cpp
src/tactic/fd_solver/fd_solver.cpp
src/sat/sat_solver/inc_sat_solver.cpp
src/qe/qe_sat_tactic.cpp
src/qe/qe_mbi.cpp
src/qe/qe_lite.cpp
src/qe/qe_tactic.cpp
src/tactic/sls/sls_tactic.cpp
src/tactic/sls/sls_engine.cpp
src/smt/tactic/ctx_solver_simplify_tactic.cpp
src/smt/tactic/smt_tactic.cpp
src/tactic/bv/bv1_blaster_tactic.cpp
src/tactic/bv/bv_size_reduction_tactic.cpp
src/tactic/bv/bv_bound_chk_tactic.cpp
src/tactic/bv/bv_bounds_tactic.cpp
src/tactic/bv/elim_small_bv_tactic.cpp
src/tactic/bv/bvarray2uf_tactic.cpp
src/tactic/bv/max_bv_sharing_tactic.cpp
src/tactic/bv/bvarray2uf_rewriter.cpp
src/tactic/bv/dt2bv_tactic.cpp
src/tactic/bv/bit_blaster_tactic.cpp
src/smt/smt_implied_equalities.cpp
src/smt/asserted_formulas.cpp
src/smt/smt_solver.cpp
src/ackermannization/ackr_bound_probe.cpp
src/ackermannization/lackr.cpp
src/tactic/aig/aig_tactic.cpp
src/math/subpaving/tactic/subpaving_tactic.cpp
src/nlsat/tactic/goal2nlsat.cpp
src/nlsat/tactic/qfnra_nlsat_tactic.cpp
src/nlsat/tactic/nlsat_tactic.cpp
src/tactic/arith/recover_01_tactic.cpp
src/tactic/arith/diff_neq_tactic.cpp
src/tactic/arith/card2bv_tactic.cpp
src/tactic/arith/lia2card_tactic.cpp
src/tactic/arith/pb2bv_tactic.cpp
src/tactic/arith/factor_tactic.cpp
src/tactic/arith/purify_arith_tactic.cpp
src/tactic/arith/fm_tactic.cpp
src/tactic/arith/nla2bv_tactic.cpp
src/tactic/arith/add_bounds_tactic.cpp
src/tactic/arith/lia2pb_tactic.cpp
src/tactic/arith/eq2bv_tactic.cpp
src/tactic/arith/arith_bounds_tactic.cpp
src/tactic/arith/propagate_ineqs_tactic.cpp
src/tactic/arith/degree_shift_tactic.cpp
src/tactic/arith/fix_dl_var_tactic.cpp
src/tactic/arith/normalize_bounds_tactic.cpp
src/tactic/core/reduce_args_tactic.cpp
src/tactic/core/cofactor_elim_term_ite.cpp
src/tactic/core/nnf_tactic.cpp
src/tactic/core/split_clause_tactic.cpp
src/tactic/core/special_relations_tactic.cpp
src/tactic/core/collect_statistics_tactic.cpp
src/tactic/core/cofactor_term_ite_tactic.cpp
src/tactic/core/simplify_tactic.cpp
src/tactic/core/der_tactic.cpp
src/tactic/core/pb_preprocess_tactic.cpp
src/tactic/core/symmetry_reduce_tactic.cpp
src/tactic/core/elim_term_ite_tactic.cpp
src/tactic/core/solve_eqs_tactic.cpp
src/tactic/core/elim_uncnstr_tactic.cpp
src/tactic/core/distribute_forall_tactic.cpp
src/tactic/core/occf_tactic.cpp
src/tactic/core/reduce_invertible_tactic.cpp
src/tactic/core/dom_simplify_tactic.cpp
src/tactic/core/propagate_values_tactic.cpp
src/tactic/core/blast_term_ite_tactic.cpp
src/tactic/core/injectivity_tactic.cpp
src/tactic/core/ctx_simplify_tactic.cpp
src/tactic/core/tseitin_cnf_tactic.cpp
src/sat/tactic/sat_tactic.cpp
src/sat/tactic/goal2sat.cpp
src/cmd_context/context_params.cpp
src/solver/tactic2solver.cpp
src/solver/mus.cpp
src/solver/solver_na2as.cpp
src/solver/solver2tactic.cpp
src/solver/parallel_tactic.cpp
src/solver/solver_pool.cpp
src/solver/combined_solver.cpp
src/solver/solver.cpp
src/tactic/tactic.cpp
src/tactic/tactical.cpp
src/tactic/sine_filter.cpp
src/cmd_context/extra_cmds/polynomial_cmds.cpp
src/cmd_context/extra_cmds/subpaving_cmds.cpp
src/cmd_context/extra_cmds/dbg_cmds.cpp
src/tactic/fpa/qffp_tactic.cpp
src/tactic/smtlogics/qfbv_tactic.cpp
src/tactic/smtlogics/qfufbv_tactic.cpp
src/tactic/smtlogics/quant_tactics.cpp
src/tactic/smtlogics/qfaufbv_tactic.cpp
src/muz/spacer/spacer_util.cpp
src/muz/spacer/spacer_legacy_mbp.cpp
src/muz/spacer/spacer_manager.cpp
src/muz/spacer/spacer_legacy_mev.cpp
src/muz/spacer/spacer_prop_solver.cpp
src/qe/nlqsat.cpp
src/qe/qe.cpp
src/qe/qsat.cpp
src/qe/qe_cmd.cpp
src/tactic/sls/bvsls_opt_engine.cpp
src/smt/tactic/unit_subsumption_tactic.cpp
src/smt/smt_lookahead.cpp
src/smt/smt_context_stat.cpp
src/smt/smt_quick_checker.cpp
src/smt/smt_context_pp.cpp
src/smt/smt_conflict_resolution.cpp
src/smt/theory_datatype.cpp
src/smt/smt_theory.cpp
src/smt/smt_quantifier.cpp
src/smt/smt_clause_proof.cpp
src/smt/smt_for_each_relevant_expr.cpp
src/smt/smt_relevancy.cpp
src/smt/theory_array_base.cpp
src/smt/smt_case_split_queue.cpp
src/smt/arith_eq_adapter.cpp
src/smt/theory_pb.cpp
src/smt/smt_model_finder.cpp
src/smt/qi_queue.cpp
src/smt/theory_special_relations.cpp
src/smt/theory_dummy.cpp
src/smt/theory_seq.cpp
src/smt/smt_context_inv.cpp
src/smt/theory_fpa.cpp
src/smt/theory_bv.cpp
src/smt/smt_arith_value.cpp
src/smt/theory_array_full.cpp
src/smt/smt_context.cpp
src/smt/dyn_ack.cpp
src/smt/theory_wmaxsat.cpp
src/smt/mam.cpp
src/smt/smt_internalizer.cpp
src/smt/smt_justification.cpp
src/smt/theory_array.cpp
src/smt/smt_consequences.cpp
src/smt/smt_checker.cpp
src/smt/smt_model_generator.cpp
src/smt/theory_jobscheduler.cpp
src/smt/smt_enode.cpp
src/smt/theory_recfun.cpp
src/smt/theory_dl.cpp
src/smt/smt_kernel.cpp
src/smt/smt_model_checker.cpp
src/smt/theory_array_bapa.cpp
src/ackermannization/ackermannize_bv_tactic.cpp
src/cmd_context/echo_tactic.cpp
src/cmd_context/basic_cmds.cpp
src/cmd_context/cmd_context_to_goal.cpp
src/cmd_context/cmd_context.cpp
src/cmd_context/cmd_util.cpp
src/cmd_context/tactic_cmds.cpp
src/cmd_context/parametric_cmd.cpp
src/cmd_context/eval_cmd.cpp
src/cmd_context/simplify_cmd.cpp
src/util/lp/row_eta_matrix.cpp
src/util/lp/square_dense_submatrix.cpp
src/util/lp/square_sparse_matrix.cpp
src/api/dll/install_tactic.cpp
src/shell/install_tactic.cpp
src/api/api_special_relations.cpp
src/api/api_qe.cpp
src/api/api_bv.cpp
src/api/api_ast_map.cpp
src/api/api_tactic.cpp
src/api/api_model.cpp
src/api/api_quant.cpp
src/api/api_params.cpp
src/api/api_context.cpp
src/api/api_ast.cpp
src/api/api_ast_vector.cpp
src/api/api_config_params.cpp
src/api/api_array.cpp
src/api/api_fpa.cpp
src/api/api_numeral.cpp
src/api/api_solver.cpp
src/api/api_arith.cpp
src/api/api_pb.cpp
src/api/api_seq.cpp
src/api/api_polynomial.cpp
src/api/api_goal.cpp
src/api/api_datatype.cpp
src/api/api_parsers.cpp
src/api/api_algebraic.cpp
src/api/api_rcf.cpp
src/api/api_stats.cpp
src/tactic/portfolio/smt_strategic_solver.cpp
src/muz/dataflow/dataflow.cpp
src/smt/theory_diff_logic.cpp
src/smt/smt2_extra_cmds.cpp
src/smt/smt_setup.cpp
src/smt/theory_utvpi.cpp
src/smt/theory_str_regex.cpp
src/ast/pattern/expr_pattern_match.cpp
src/parsers/smt2/smt2scanner.cpp
src/parsers/smt2/marshal.cpp
src/parsers/smt2/smt2parser.cpp
src/util/lp/lu.cpp
src/opt/sortmax.cpp
src/opt/maxlex.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/wmax.cpp
src/opt/maxres.cpp
src/muz/fp/datalog_parser.cpp
src/muz/ddnf/ddnf.cpp
src/muz/clp/clp_context.cpp
src/muz/spacer/spacer_quant_generalizer.cpp
src/muz/spacer/spacer_arith_generalizers.cpp
src/muz/spacer/spacer_json.cpp
src/muz/spacer/spacer_sat_answer.cpp
src/muz/transforms/dl_mk_karr_invariants.cpp
src/muz/transforms/dl_mk_quantifier_instantiation.cpp
src/muz/transforms/dl_mk_bit_blast.cpp
src/muz/transforms/dl_mk_scale.cpp
src/muz/transforms/dl_mk_coi_filter.cpp
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
src/muz/transforms/dl_mk_magic_symbolic.cpp
src/muz/transforms/dl_mk_array_eq_rewrite.cpp
src/muz/transforms/dl_mk_magic_sets.cpp
src/muz/transforms/dl_mk_loop_counter.cpp
src/muz/transforms/dl_mk_array_instantiation.cpp
src/muz/transforms/dl_mk_filter_rules.cpp
src/muz/transforms/dl_mk_backwards.cpp
src/muz/transforms/dl_mk_unbound_compressor.cpp
src/muz/transforms/dl_mk_separate_negated_tails.cpp
src/muz/base/rule_properties.cpp
src/muz/base/dl_rule_set.cpp
src/muz/base/dl_costs.cpp
src/muz/base/dl_rule.cpp
src/muz/base/dl_rule_transformer.cpp
src/muz/base/dl_util.cpp
src/muz/base/dl_rule_subsumption_index.cpp
src/muz/base/dl_context.cpp
src/smt/theory_dense_diff_logic.cpp
src/smt/theory_str.cpp
src/smt/theory_arith.cpp
src/util/lp/core_solver_pretty_printer.cpp
src/util/lp/lp_core_solver_base.cpp
src/shell/opt_frontend.cpp
src/api/api_opt.cpp
src/opt/opt_cmds.cpp
src/muz/fp/horn_tactic.cpp
src/muz/tab/tab_context.cpp
src/muz/spacer/spacer_generalizers.cpp
src/muz/spacer/spacer_context.cpp
src/muz/spacer/spacer_legacy_frames.cpp
src/muz/spacer/spacer_callback.cpp
src/muz/spacer/spacer_pdr.cpp
src/muz/rel/dl_external_relation.cpp
src/muz/rel/dl_sparse_table.cpp
src/muz/transforms/dl_mk_subsumption_checker.cpp
src/muz/transforms/dl_mk_slice.cpp
src/muz/transforms/dl_mk_array_blast.cpp
src/muz/transforms/dl_mk_unfold.cpp
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
src/muz/transforms/dl_mk_coalesce.cpp
src/muz/transforms/dl_mk_elim_term_ite.cpp
src/muz/transforms/dl_mk_rule_inliner.cpp
src/muz/transforms/dl_transforms.cpp
src/util/lp/lp_dual_core_solver.cpp
src/util/lp/lp_solver.cpp
src/shell/smtlib_frontend.cpp
src/api/api_datalog.cpp
src/muz/fp/dl_register_engine.cpp
src/muz/bmc/dl_bmc_engine.cpp
src/muz/spacer/spacer_dl_interface.cpp
src/muz/rel/dl_table_relation.cpp
src/muz/rel/check_relation.cpp
src/muz/rel/dl_mk_similarity_compressor.cpp
src/muz/rel/dl_mk_simple_joins.cpp
src/muz/rel/karr_relation.cpp
src/muz/rel/dl_lazy_table.cpp
src/muz/rel/dl_base.cpp
src/muz/rel/dl_table.cpp
src/muz/rel/dl_instruction.cpp
src/muz/rel/dl_bound_relation.cpp
src/muz/rel/udoc_relation.cpp
src/muz/rel/dl_sieve_relation.cpp
src/muz/transforms/dl_mk_synchronize.cpp
src/smt/theory_lra.cpp
src/util/lp/int_solver.cpp
src/util/lp/static_matrix.cpp
src/util/lp/gomory.cpp
src/util/lp/nra_solver.cpp
src/util/lp/lp_primal_core_solver.cpp
src/util/lp/lar_solver.cpp
src/util/lp/lp_dual_simplex.cpp
src/util/lp/lp_bound_propagator.cpp
src/util/lp/lar_core_solver.cpp
src/muz/fp/dl_cmds.cpp
src/muz/rel/dl_interval_relation.cpp
src/muz/rel/dl_product_relation.cpp
src/muz/rel/aig_exporter.cpp
src/muz/rel/dl_finite_product_relation.cpp
src/muz/rel/rel_context.cpp
src/muz/rel/dl_check_table.cpp
src/muz/rel/dl_relation_manager.cpp
src/muz/rel/dl_compiler.cpp
src/muz/rel/dl_mk_explanations.cpp
src/util/lp/random_updater.cpp
src/util/lp/lp_primal_simplex.cpp
src/shell/datalog_frontend.cpp
src/shell/lp_frontend.cpp
g++ -o libz3.so -shared api/dll/gparams_register_modules.o api/dll/dll.o api/dll/mem_initializer.o api/dll/install_tactic.o api/api_special_relations.o api/api_commands.o api/api_qe.o api/api_bv.o api/api_ast_map.o api/api_tactic.o api/api_model.o api/api_quant.o api/api_log.o api/api_params.o api/api_context.o api/api_ast.o api/api_ast_vector.o api/api_config_params.o api/api_array.o api/api_fpa.o api/api_log_macros.o api/api_numeral.o api/api_solver.o api/api_opt.o api/api_arith.o api/api_pb.o api/api_seq.o api/api_polynomial.o api/api_datalog.o api/api_goal.o api/api_datatype.o api/api_parsers.o api/api_algebraic.o api/api_rcf.o api/api_stats.o api/z3_replayer.o cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a tactic/ufbv/ufbv_tactic.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 smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/pattern/pattern.a parsers/smt2/smt2parser.a sat/tactic/sat_tactic.a cmd_context/cmd_context.a solver/solver.a ast/proofs/proofs.a math/euclid/euclid.a math/grobner/grobner.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 ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/automata/automata.a math/simplex/simplex.a math/hilbert/hilbert.a util/lp/lp.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -lpthread  -Wl,-soname,libz3.so
ln -f -s ../libz3.so python
g++  -o z3  shell/smtlib_frontend.o shell/main.o shell/dimacs_frontend.o shell/z3_log_frontend.o shell/gparams_register_modules.o shell/opt_frontend.o shell/datalog_frontend.o shell/mem_initializer.o shell/install_tactic.o shell/lp_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/smtlogics/smtlogic_tactics.a tactic/ufbv/ufbv_tactic.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 smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/pattern/pattern.a parsers/smt2/smt2parser.a sat/tactic/sat_tactic.a cmd_context/cmd_context.a solver/solver.a ast/proofs/proofs.a math/euclid/euclid.a math/grobner/grobner.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 ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/automata/automata.a math/simplex/simplex.a math/hilbert/hilbert.a util/lp/lp.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -lpthread 
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
Z3 was successfully installed.
Removing intermediate container 94512d2c6fd6
 ---> 378fd1970e03
Step 4/10 : USER user:user
 ---> Running in 8a2ed40a6d29
Removing intermediate container 8a2ed40a6d29
 ---> 97123e8a6972
Step 5/10 : COPY --from=runtimeverificationinc/perl:ubuntu-bionic      --chown=user:user      /home/user/perl5      /home/user/perl5
ubuntu-bionic: Pulling from runtimeverificationinc/perl
7413c47ba209: Already exists
0fe7e7cbb2e8: Already exists
1d425c982345: Already exists
344da5c95cec: Already exists
168a746b665d: Pulling fs layer
959fe92c399b: Pulling fs layer
274f166424f6: Pulling fs layer
7f66b81925c6: Pulling fs layer
54e94f2a5421: Pulling fs layer
defbeebc3b50: Pulling fs layer
7f66b81925c6: Waiting
defbeebc3b50: Waiting
54e94f2a5421: Waiting
168a746b665d: Download complete
168a746b665d: Pull complete
7f66b81925c6: Verifying Checksum
7f66b81925c6: Download complete
274f166424f6: Verifying Checksum
274f166424f6: Download complete
959fe92c399b: Verifying Checksum
959fe92c399b: Download complete
defbeebc3b50: Download complete
54e94f2a5421: Verifying Checksum
54e94f2a5421: Download complete
959fe92c399b: Pull complete
274f166424f6: Pull complete
7f66b81925c6: Pull complete
54e94f2a5421: Pull complete
defbeebc3b50: Pull complete
Digest: sha256:a7400f90cc8a5449e5d5f0cafe4a0b4b43d74fcc5c83eb4b2a8a421ba5cc7d11
Status: Downloaded newer image for runtimeverificationinc/perl:ubuntu-bionic
 ---> f825bbd64cee
Step 6/10 : COPY --from=runtimeverificationinc/ocaml:ubuntu-bionic      --chown=user:user      /home/user/.opam      /home/user/.opam
ubuntu-bionic: Pulling from runtimeverificationinc/ocaml
7413c47ba209: Already exists
0fe7e7cbb2e8: Already exists
1d425c982345: Already exists
344da5c95cec: Already exists
168a746b665d: Already exists
959fe92c399b: Already exists
274f166424f6: Already exists
7f66b81925c6: Already exists
5b27be4a3fd4: Pulling fs layer
5f8e31c70517: Pulling fs layer
324d9497116f: Pulling fs layer
5f8e31c70517: Verifying Checksum
5f8e31c70517: Download complete
324d9497116f: Verifying Checksum
324d9497116f: Download complete
5b27be4a3fd4: Verifying Checksum
5b27be4a3fd4: Download complete
5b27be4a3fd4: Pull complete
5f8e31c70517: Pull complete
324d9497116f: Pull complete
Digest: sha256:cdb6dc072777816beaa5b9f07d159c46ba52a6f2d660ea5da8585b5c1d0bf694
Status: Downloaded newer image for runtimeverificationinc/ocaml:ubuntu-bionic
 ---> 2dfc02926423
Step 7/10 : ENV DEPS_DIR="/home/user/c-semantics-deps"
 ---> Running in ddcc42571422
Removing intermediate container ddcc42571422
 ---> 382c13be9b16
Step 8/10 : COPY --chown=user:user ./.build/k/ ${DEPS_DIR}/k
 ---> 7ca10d1d235e
Step 9/10 : RUN cd ${DEPS_DIR}/k   && mvn package -q -U       -DskipTests -DskipKTest       -Dhaskell.backend.skip -Dllvm.backend.skip       -Dcheckstyle.skip
 ---> Running in cd149f336304
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/usr/share/maven/lib/guice.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of com.google.inject.internal.cglib.core.$ReflectUtils$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
Java Compiler Compiler Version 5.0 (Parser Generator)
(type "javacc" with no arguments for help)
Reading from file /home/user/c-semantics-deps/k/kernel/src/main/javacc/KastParser.jj . . .
Note: UNICODE_INPUT option is specified. Please make sure you create the parser/lexer using a Reader with the correct character encoding.
File "TokenMgrError.java" does not exist.  Will create one.
File "ParseException.java" does not exist.  Will create one.
File "Token.java" does not exist.  Will create one.
File "SimpleCharStream.java" does not exist.  Will create one.
Parser generated successfully.
Java Compiler Compiler Version 5.0 (Parser Generator)
(type "javacc" with no arguments for help)
Reading from file /home/user/c-semantics-deps/k/kernel/src/main/javacc/Outer.jj . . .
Note: UNICODE_INPUT option is specified. Please make sure you create the parser/lexer using a Reader with the correct character encoding.
Warning: Line 713, Column 3: Regular expression for GROUP can be matched by the empty string ("") in lexical state GROUP_STATE. This can result in an endless loop of empty string matches.
File "TokenMgrError.java" does not exist.  Will create one.
File "ParseException.java" does not exist.  Will create one.
File "Token.java" does not exist.  Will create one.
File "SimpleCharStream.java" does not exist.  Will create one.
Parser generated with 0 errors and 1 warnings.
Java Compiler Compiler Version 5.0 (Parser Generator)
(type "javacc" with no arguments for help)
Reading from file /home/user/c-semantics-deps/k/kernel/src/main/javacc/SmtSortParser.jj . . .
File "TokenMgrError.java" does not exist.  Will create one.
File "ParseException.java" does not exist.  Will create one.
File "Token.java" does not exist.  Will create one.
File "SimpleCharStream.java" does not exist.  Will create one.
Parser generated successfully.
Removing intermediate container cd149f336304
 ---> b2cdcbabab10
Step 10/10 : ENV K_BIN="${DEPS_DIR}/k/k-distribution/target/release/k/bin"
 ---> Running in 87bf75bfe819
Removing intermediate container 87bf75bfe819
 ---> e427f2c65656
Successfully built e427f2c65656
Successfully tagged runtimeverificationinc/c-semantics:latest
[Pipeline] }
[Pipeline] // script
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Push to dockerhub)
[Pipeline] script
[Pipeline] {
[Pipeline] withEnv
[Pipeline] {
[Pipeline] withDockerRegistry
$ docker login -u rvdockerhub -p ******** https://index.docker.io/v1/
WARNING! Using --password via the CLI is insecure. Use --password-stdin.
WARNING! Your password will be stored unencrypted in /home/jenkins-slave/workspace/c-semantics_master@tmp/0ee0b090-742c-4fc8-8448-cd2a5d5db66f/config.json.
Configure a credential helper to remove this warning. See
https://docs.docker.com/engine/reference/commandline/login/#credentials-store

Login Succeeded
[Pipeline] {
[Pipeline] sh
+ docker tag runtimeverificationinc/c-semantics:latest runtimeverificationinc/c-semantics:latest
[Pipeline] sh
+ docker push runtimeverificationinc/c-semantics:latest
The push refers to repository [docker.io/runtimeverificationinc/c-semantics]
77e489053d71: Preparing
21d1b9d035c1: Preparing
57bd3900e82e: Preparing
1c54343348cf: Preparing
390ca046e724: Preparing
3d25263d3363: Preparing
f0cced769d57: Preparing
c5d7137d5271: Preparing
3fb6d93b94dc: Preparing
b2ebe198c4c0: Preparing
6b08a96cd75a: Preparing
7f561a103d7a: Preparing
b079b3fa8d1b: Preparing
a31dbd3063d7: Preparing
c56e09e1bd18: Preparing
543791078bdb: Preparing
b2ebe198c4c0: Waiting
3d25263d3363: Waiting
6b08a96cd75a: Waiting
7f561a103d7a: Waiting
c56e09e1bd18: Waiting
3fb6d93b94dc: Waiting
b079b3fa8d1b: Waiting
f0cced769d57: Waiting
543791078bdb: Waiting
c5d7137d5271: Waiting
a31dbd3063d7: Waiting
1c54343348cf: Pushed
21d1b9d035c1: Pushed
f0cced769d57: Layer already exists
c5d7137d5271: Layer already exists
3fb6d93b94dc: Layer already exists
b2ebe198c4c0: Layer already exists
6b08a96cd75a: Layer already exists
7f561a103d7a: Layer already exists
390ca046e724: Pushed
b079b3fa8d1b: Layer already exists
a31dbd3063d7: Layer already exists
c56e09e1bd18: Layer already exists
543791078bdb: Layer already exists
77e489053d71: Pushed
3d25263d3363: Pushed
57bd3900e82e: Pushed
latest: digest: sha256:5118a45b36a8a17f468c14b1260450ccc8a93f6980c9085dd4b3dc85a04baa54 size: 3686
[Pipeline] }
[Pipeline] // withDockerRegistry
[Pipeline] }
[Pipeline] // withEnv
[Pipeline] }
[Pipeline] // script
[Pipeline] }
[Pipeline] // stage
[Pipeline] }
[Pipeline] // withEnv
[Pipeline] }
[Pipeline] // node
[Pipeline] }
[Pipeline] // stage
[Pipeline] }
[Pipeline] // ansiColor
[Pipeline] End of Pipeline

GitHub has been notified of this commit’s build result

Finished: SUCCESS