hgvk94 / z3 Goto Github PK

This project forked from z3prover/z3

The Z3 Theorem Prover

License: Other

CMake 0.68% C++ 88.15% Dockerfile 0.01% Shell 0.01% Python 3.10% Makefile 0.01% Batchfile 0.01% C 1.89% C# 2.48% Java 1.63% OCaml 0.93% SMT 0.13% TypeScript 0.93% JavaScript 0.01% D 0.06%

z3's Introduction

Z3

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.

If you are not familiar with Z3, you can start here.

Pre-built binaries for stable and nightly releases are available from here.

Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages.

See the release notes for notes on various stable releases of Z3.

Build status

Azure Pipelines	Code Coverage	Open Bugs	Android Build	WASM Build

Docker image.

Building Z3 on Windows using Visual Studio Command Prompt

32-bit builds, start with:

python scripts/mk_make.py

or instead, for a 64-bit build:

python scripts/mk_make.py -x

then:

cd build
nmake

Z3 uses C++17. The recommended version of Visual Studio is therefore VS2019.

Building Z3 using make and GCC/Clang

Execute:

python scripts/mk_make.py
cd build
make
sudo make install

Note by default g++ is used as the C++ compiler if it is available. If you would prefer to use Clang change the mk_make.py invocation to:

CXX=clang++ CC=clang python scripts/mk_make.py

Note that Clang < 3.7 does not support OpenMP.

You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler. To configure that case correctly, make sure to use Cygwin's own python and not some Windows installation of Python.

For a 64 bit build (from Cygwin64), configure Z3's sources with

CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py

A 32 bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32.

By default, it will install z3 executable at PREFIX/bin, libraries at PREFIX/lib, and include files at PREFIX/include, where PREFIX installation prefix is inferred by the mk_make.py script. It is usually /usr for most Linux distros, and /usr/local for FreeBSD and macOS. Use the --prefix= command line option to change the install prefix. For example:

python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install

To uninstall Z3, use

sudo make uninstall

To clean Z3 you can delete the build directory and run the mk_make.py script again.

Building Z3 using CMake

Z3 has a build system using CMake. Read the README-CMake.md file for details. It is recommended for most build tasks, except for building OCaml bindings.

Building Z3 using vcpkg

vcpkg is a full platform package manager, you can easily install libzmq with vcpkg.

Execute:

git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3

Dependencies

Z3 itself has few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading. It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained multi-precision functionality. Python is required to build Z3. To build Java, .Net, OCaml, Julia APIs requires installing relevant tool chains.

Z3 bindings

Z3 has bindings for various programming languages.

`.NET`

You can install a nuget package for the latest release Z3 from nuget.org.

Use the --dotnet command line flag with mk_make.py to enable building these.

See examples/dotnet for examples.

`C`

These are always enabled.

See examples/c for examples.

`C++`

These are always enabled.

See examples/c++ for examples.

`Java`

Use the --java command line flag with mk_make.py to enable building these.

See examples/java for examples.

`OCaml`

Use the --ml command line flag with mk_make.py to enable building these.

See examples/ml for examples.

`Python`

You can install the Python wrapper for Z3 for the latest release from pypi using the command

   pip install z3-solver

Use the --python command line flag with mk_make.py to enable building these.

Note that it is required on certain platforms that the Python package directory (site-packages on most distributions and dist-packages on Debian based distributions) live under the install prefix. If you use a non standard prefix you can use the --pypkgdir option to change the Python package directory used for installation. For example:

python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages

If you do need to install to a non standard prefix a better approach is to use a Python virtual environment and install Z3 there. Python packages also work for Python3. Under Windows, recall to build inside the Visual C++ native command build environment. Note that the build/python/z3 directory should be accessible from where python is used with Z3 and it depends on libz3.dll to be in the path.

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

See examples/python for examples.

`Julia`

The Julia package Z3.jl wraps the C++ API of Z3. Information about updating and building the Julia bindings can be found in src/api/julia.

`Web Assembly` / `TypeScript` / `JavaScript`

A WebAssembly build with associated TypeScript typings is published on npm as z3-solver. Information about building these bindings can be found in src/api/js.

Smalltalk (`Pharo` / `Smalltalk/X`)

Project MachineArithmetic provides Smalltalk interface to Z3's C API. For more information, see MachineArithmetic/README.md

System Overview

Interfaces

Default input format is SMTLIB2
Other native foreign function interfaces:
C++ API
.NET API
Java API
Python API (also available in pydoc format)
C
OCaml
Julia
Smalltalk (supports Pharo and Smalltalk/X)

z3's People

Contributors

Stargazers

Watchers

Forkers

tomasmachacekw a-hamza-r lvzc0

z3's Issues

Unsoundness with mk_slice transform

instance
commit
options: fp.xform.slice=true
The instance is sat but Z3 says unsat when slicing is enabled.

Is there a command to invoke MBP directly?

I want to apply MBP to BV formula (in smtlib)，and I wonder if there exists such a command to call mbp directly. Thank you.

issue with slicing

commit
instance
Issue:
The instance is SAT. If Z3 is run with argument fp.xform.slice=true, Z3 will say UNSAT. If run with the argument fp.xform.slice=false, Z3 will say SAT.
Cause:
The 3rd argument to Inv is not slicable because it is being used in the formula. However, Z3 thinks it is slicable and removes it from Inv. This makes the formula unsatisfiabe.

Another observation is that removing the clause (=> false false) gets rid of the bug. That is, if you remove this clause from the formula, Z3 does not slice the formula.

seg fault while reducing proof inside iuc solver

commit: 20184ea csmbv origin/csmbv use model completion during expr eval
command: ./z3 hongce/aes0.smt2 fp.engine=spacer
reason: signal SIGSEGV: invalid address (fault address: 0x555d581d0678)
stack trace:
frame #0: 0x0000555556718ae0 z3spacer::hypothesis_reducer::reduce_core(this=0x00007fffffffbf20, pf=0x00000000a9968901) at spacer_proof_utils.cpp:619 frame #1: 0x0000555556719477 z3spacer::hypothesis_reducer::reduce(this=0x00007fffffffbf20, pr=0x0000555557b90198) at spacer_proof_utils.cpp:474
frame #2: 0x000055555670cfae z3spacer::iuc_solver::get_iuc(this=0x000055555740db88, core=0x00007fffffffc4a0) at spacer_iuc_solver.cpp:363 frame #3: 0x00005555566dc848 z3spacer::prop_solver::internal_check_assumptions(this=0x0000555556fc5698, hard_atoms=, soft_atoms=, clauses=) at spacer_prop_solver.cpp:336
frame #4: 0x00005555566dcb85 z3spacer::prop_solver::check_assumptions(this=0x0000555556fc5698, _hard=<unavailable>, soft=0x00007fffffffc350, clause=0x00005555572e3b10, num_bg=1, bg=0x00007fffffffc320, solver_id=0) at spacer_prop_solver.cpp:385 frame #5: 0x00005555566a9792 z3spacer::pred_transformer::is_reachable(this=0x00005555572e3a28, n=, core=0x00007fffffffc4a0, model=0x00007fffffffc458, uses_level=0x00007fffffffc450, is_concrete=0x00007fffffffc44f, r=0x00007fffffffc460, reach_pred_used=0x00007fffffffc468, num_reuse_reach=0x00007fffffffc454, use_iuc=true) at spacer_context.cpp:1458
frame #6: 0x00005555566bc5d4 z3spacer::context::expand_pob(this=0x0000555557180978, n=0x00005555577bfc98, out=0x00007fffffffc600) at spacer_context.cpp:3555 frame #7: 0x00005555566c0211 z3spacer::context::check_reachability(this=0x0000555557180978) at spacer_context.cpp:3196
frame #8: 0x00005555566c3910 z3spacer::context::solve_core(this=0x0000555557180978, from_lvl=<unavailable>) at spacer_context.cpp:3084 frame #9: 0x00005555566c3e75 z3spacer::context::solve(this=0x0000555557180978, from_lvl=) at spacer_context.cpp:2769
frame #10: 0x00005555566cbb22 z3spacer::dl_interface::query(this=0x00005555571ceeb8, query=<unavailable>) at spacer_dl_interface.cpp:167 frame #11: 0x0000555556656ead z3datalog::engine_base::query(this=0x00005555571ceeb8, num_rels=, rels=) at dl_engine_base.h:71
frame Z3Prover#12: 0x00005555567d49d6 z3dl_query_cmd::execute(this=0x0000555556e667a8, ctx=0x00007fffffffd970) at dl_cmds.cpp:260 frame #13: 0x0000555555e39b75 z3smt2::parser::parse_ext_cmd(this=0x00007fffffffce90, line=, pos=0) at smt2parser.cpp:2920
frame Z3Prover#14: 0x0000555555e3d074 z3smt2::parser::operator()() at smt2parser.cpp:3026 frame #15: 0x0000555555e3cf50 z3smt2::parser::operator(this=0x00007fffffffce90)() at smt2parser.cpp:3138
frame Z3Prover#16: 0x0000555555e25c13 z3parse_smt2_commands(ctx=0x00007fffffffd970, is=0x00007fffffffd760, interactive=<unavailable>, ps=<unavailable>, filename=0x0000000000000000) at smt2parser.cpp:3187 frame #17: 0x000055555690993e z3read_smtlib2_commands(file_name=) at smtlib_frontend.cpp:95
frame Z3Prover#18: 0x00005555555e5332 z3main(argc=<unavailable>, argv=<unavailable>) at main.cpp:353 frame #19: 0x00007ffff6c78b97 libc.so.6__libc_start_main(main=(z3main at main.cpp:298), argc=6, argv=0x00007fffffffddf8, init=<unavailable>, fini=<unavailable>, rtld_fini=<unavailable>, stack_end=0x00007fffffffdde8) at libc-start.c:310 frame #20: 0x00005555555e575a z3_start + 42

MBP reports error "could not evaluate Boolean in model"

I tried mbp command in an example gen35.smt2.zip , it reports "could not evaluate Boolean in model".

sat
(error "line 37 column 105819: could not evaluate Boolean in model")

I add (get-model) between (check-sat) and mbp，then it seems to output normally.

sat...

sat
(
  (define-fun input11 () (_ BitVec 1)
    #b0)
  (define-fun input5 () (_ BitVec 1)
    #b0)
  (define-fun input9 () (_ BitVec 1)
    #b0)
  (define-fun state90.next () (_ BitVec 1)
    #b1)
  (define-fun input2 () (_ BitVec 1)
    #b0)
  (define-fun state63_nn () (_ BitVec 1)
    #b1)
  (define-fun state90_nn () (_ BitVec 1)
    #b0)
  (define-fun state63.next () (_ BitVec 1)
    #b0)
  (define-fun state90 () (_ BitVec 1)
    #b1)
  (define-fun state20.next () (_ BitVec 256)
    #x0000000000000000000000000000000000000000000000000000000000000000)
  (define-fun _monitor_0.next () Bool
    true)
  (define-fun state61.next () (_ BitVec 1)
    #b0)
  (define-fun state22.next () (_ BitVec 512)
    #x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
  (define-fun input6 () (_ BitVec 1)
    #b1)
  (define-fun _monitor_0 () Bool
    true)
  (define-fun state61_nn () (_ BitVec 1)
    #b0)
  (define-fun state20_nn () (_ BitVec 256)
    #x0000000000000000000000000000000000000000000000000000000000000000)
  (define-fun state22_nn () (_ BitVec 512)
    #x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
  (define-fun state22 () (_ BitVec 512)
    #x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
  (define-fun _monitor_0_nn () Bool
    true)
  (define-fun state61 () (_ BitVec 1)
    #b0)
  (define-fun state63 () (_ BitVec 1)
    #b0)
  (define-fun state20 () (_ BitVec 256)
    #x0000000000000000000000000000000000000000000000000000000000000000)
  (define-fun input8 () (_ BitVec 2)
    #b11)
  (define-fun input3 () (_ BitVec 1)
    #b1)
  (define-fun input17 () (_ BitVec 1)
    #b0)
  (define-fun input18 () (_ BitVec 1)
    #b0)
  (define-fun input16 () (_ BitVec 1)
    #b0)
  (define-fun input14 () (_ BitVec 1)
    #b0)
  (define-fun input10 () (_ BitVec 1)
    #b0)
  (define-fun input15 () (_ BitVec 1)
    #b0)
  (define-fun input4 () (_ BitVec 1)
    #b0)
  (define-fun input13 () (_ BitVec 279)
    #b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)
(let ((a!1 (bvor (bvnot (bvor (bvnot input5) input6)) (bvnot input6) input2)))
  (and (= state20_nn
          #x0000000000000000000000000000000000000000000000000000000000000000)
       (= state61_nn #b0)
       _monitor_0_nn
       (= input8 #b11)
       (= state22_nn
          #x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
       (not (= input9 #b1))
       (not (= input5 #b1))
       (not (= input2 #b1))
       (not (= input11 #b1))
       (not (= input8 #b01))
       (= input6 #b1)
       (= input3 #b1)
       (= ((_ extract 282 282) state22_nn) #b0)
       (= state63_nn (bvnot a!1))
       (= state90_nn #b0)
       (= input5 #b0)
       (not (= input17 #b1))))

I wonder why it happens and if adding `(get-model)` will affect results. Thank you @hgvk94

Issue with check_sat_cc

Instance
commit
Running z3 with default options causes it to either seg fault:

    frame #0: 0x00000000016eec8b z3`smt::conflict_resolution::process_justifications(this=0x0000000002512f48) at smt_conflict_resolution.cpp:204:21
   201 	            while (m_todo_js_qhead < sz) {
   202 	                justification * js = m_todo_js[m_todo_js_qhead];
   203 	                m_todo_js_qhead++;
-> 204 	                js->get_antecedents(*this);
   205 	            }
   206 	            while (!m_todo_eqs.empty()) {
   207 	                enode_pair p = m_todo_eqs.back();
(lldb) bt
* thread #1, name = 'z3', stop reason = signal SIGSEGV: invalid address (fault address: 0xff20)
  * frame #0: 0x00000000016eec8b z3`smt::conflict_resolution::process_justifications(this=0x0000000002512f48) at smt_conflict_resolution.cpp:204:21
    frame #1: 0x00000000016eec02 z3`smt::conflict_resolution::justification2literals_core(this=0x0000000002512f48, js=0x0000000002721388, result=0x0000000002513090) at smt_conflict_resolution.cpp:195:9
    frame #2: 0x00000000016eef5c z3`smt::conflict_resolution::justification2literals(this=0x0000000002512f48, js=0x0000000002721388, result=0x0000000002513090) at smt_conflict_resolution.cpp:241:9
    frame #3: 0x00000000016ef19a z3`smt::conflict_resolution::get_justification_max_lvl(this=0x0000000002512f48, js=0x0000000002721388) at smt_conflict_resolution.cpp:264:9
    frame #4: 0x00000000016ef4cb z3`smt::conflict_resolution::get_max_lvl(this=0x0000000002512f48, consequent=(m_val = 1), js=(m_data = 0x0000000002707058)) at smt_conflict_resolution.cpp:298:33
    frame #5: 0x00000000016eff97 z3`smt::conflict_resolution::initialize_resolve(this=0x0000000002512f48, conflict=(m_data = 0x0000000002707058), not_l=(m_val = -2), js=0x00007fffffff75d8, consequent=0x00007fffffff75d0) at smt_conflict_resolution.cpp:398:31
    frame #6: 0x00000000016f2c1c z3`smt::conflict_resolution::resolve(this=0x0000000002512f48, conflict=(m_data = 0x0000000002707058), not_l=(m_val = -2)) at smt_conflict_resolution.cpp:486:14
    frame #7: 0x000000000172d840 z3`smt::context::resolve_conflict(this=0x000000000251aaa8) at smt_context.cpp:4079:36
    frame #8: 0x000000000171cddb z3`smt::context::decide_clause(this=0x000000000251aaa8) at smt_context.cpp:3320:13
    frame #9: 0x000000000171be58 z3`smt::context::decide(this=0x000000000251aaa8) at smt_context.cpp:1761:21
    frame #10: 0x000000000172b185 z3`smt::context::bounded_search(this=0x000000000251aaa8) at smt_context.cpp:3909:18
    frame #11: 0x0000000001729997 z3`smt::context::search(this=0x000000000251aaa8) at smt_context.cpp:3745:22
    frame #12: 0x000000000172a566 z3`smt::context::check(this=0x000000000251aaa8, cube=0x000000000252c6d0, clauses=0x00007fffffff8bd0) at smt_context.cpp:3650:17
    frame #13: 0x000000000177cc55 z3`smt::kernel::imp::check(this=0x000000000251aaa8, cube=0x000000000252c6d0, clause=0x00007fffffff8bd0) at smt_kernel.cpp:120:29
    frame #14: 0x000000000177bda8 z3`smt::kernel::check(this=0x000000000252c9f0, cube=0x000000000252c6d0, clauses=0x00007fffffff8bd0) at smt_kernel.cpp:336:23
    frame #15: 0x00000000017f546e z3`(anonymous namespace)::smt_solver::check_sat_cc_core(this=0x000000000252c698, cube=0x000000000252c6d0, clauses=0x00007fffffff8bd0) at smt_solver.cpp:200:30
    frame #16: 0x00000000012e06db z3`solver_na2as::check_sat_cc(this=0x000000000252c698, assumptions=0x00000000025358d0, clauses=0x00007fffffff8bd0) at solver_na2as.cpp:73:12
    frame #17: 0x00000000012e3345 z3`pool_solver::check_sat_cc_core(this=0x0000000002535898, cube=0x00000000025358d0, clauses=0x00007fffffff8bd0) at solver_pool.cpp:191:29
    frame #18: 0x00000000012e06db z3`solver_na2as::check_sat_cc(this=0x0000000002535898, assumptions=0x00000000025e0140, clauses=0x00007fffffff8bd0) at solver_na2as.cpp:73:12
    frame #19: 0x000000000210d440 z3`spacer::iuc_solver::check_sat_cc(this=0x00000000025e0098, cube=0x00007fffffff8c00, clauses=0x00007fffffff8bd0) at spacer_iuc_solver.cpp:137:37
    frame #20: 0x00000000020b0c46 z3`spacer::prop_solver::maxsmt(this=0x00000000024d67a8, hard=0x00007fffffff8c00, soft=0x00007fffffff8e50, clauses=0x00007fffffff8bd0) at spacer_prop_solver.cpp:242:24
    frame #21: 0x00000000020b1176 z3`spacer::prop_solver::internal_check_assumptions(this=0x00000000024d67a8, hard_atoms=0x00007fffffff8c00, soft_atoms=0x00007fffffff8e50, clauses=0x00007fffffff8bd0) at spacer_prop_solver.cpp:308:20
    frame #22: 0x00000000020b1a82 z3`spacer::prop_solver::check_assumptions(this=0x00000000024d67a8, _hard=0x00007fffffff9258, soft=0x00007fffffff8e50, clause=0x0000000002523470, num_bg=2, bg=0x000000000271c6b0, solver_id=1) at spacer_prop_solver.cpp:386:17
    frame #23: 0x000000000206d0fa z3`spacer::pred_transformer::check_inductive(this=0x0000000002523388, level=0, state=0x00007fffffff9258, uses_level=0x00007fffffff9334, weakness=0) at spacer_context.cpp:1553:27
    frame #24: 0x00000000020a82ab z3`spacer::lemma_bool_inductive_generalizer::operator(this=0x00000000026ad018, lemma=0x00007fffffffa7c8)(ref<spacer::lemma>&) at spacer_generalizers.cpp:97:16

or throw an assertion violation at file: src/ast/ast.cpp, line 3170:

frame #1: 0x0000000000abbbe8 z3`ast_manager::mk_unit_resolution(this=0x00000000023dab38, num_proofs=4, proofs=0x00007fffffff6cc0, new_fact=0x00000000023dd208) at ast.cpp:3170:9
    frame #2: 0x00000000016f8750 z3`smt::conflict_resolution::get_proof(this=0x0000000002537578, l=(m_val = 1), js=(m_data = 0x00000000026ef3f8)) at smt_conflict_resolution.cpp:1041:24
    frame #3: 0x00000000016f0f8e z3`smt::conflict_resolution::mk_conflict_proof(this=0x0000000002537578, conflict=(m_data = 0x00000000026ef3f8), not_l=(m_val = -2)) at smt_conflict_resolution.cpp:1327:18
    frame #4: 0x00000000016f03c7 z3`smt::conflict_resolution::initialize_resolve(this=0x0000000002537578, conflict=(m_data = 0x00000000026ef3f8), not_l=(m_val = -2), js=0x00007fffffff75a8, consequent=0x00007fffffff75a0) at smt_conflict_resolution.cpp:417:17
    frame #5: 0x00000000016f2c1c z3`smt::conflict_resolution::resolve(this=0x0000000002537578, conflict=(m_data = 0x00000000026ef3f8), not_l=(m_val = -2)) at smt_conflict_resolution.cpp:486:14
    frame #6: 0x000000000172d840 z3`smt::context::resolve_conflict(this=0x000000000251e6e8) at smt_context.cpp:4079:36
    frame #7: 0x000000000171cddb z3`smt::context::decide_clause(this=0x000000000251e6e8) at smt_context.cpp:3320:13
    frame #8: 0x000000000171be58 z3`smt::context::decide(this=0x000000000251e6e8) at smt_context.cpp:1761:21
    frame #9: 0x000000000172b185 z3`smt::context::bounded_search(this=0x000000000251e6e8) at smt_context.cpp:3909:18
    frame #10: 0x0000000001729997 z3`smt::context::search(this=0x000000000251e6e8) at smt_context.cpp:3745:22
    frame #11: 0x000000000172a566 z3`smt::context::check(this=0x000000000251e6e8, cube=0x000000000251b8a0, clauses=0x00007fffffff8ba0) at smt_context.cpp:3650:17
    frame #12: 0x000000000177cc55 z3`smt::kernel::imp::check(this=0x000000000251e6e8, cube=0x000000000251b8a0, clause=0x00007fffffff8ba0) at smt_kernel.cpp:120:29
    frame #13: 0x000000000177bda8 z3`smt::kernel::check(this=0x000000000251bbc0, cube=0x000000000251b8a0, clauses=0x00007fffffff8ba0) at smt_kernel.cpp:336:23
    frame #14: 0x00000000017f546e z3`(anonymous namespace)::smt_solver::check_sat_cc_core(this=0x000000000251b868, cube=0x000000000251b8a0, clauses=0x00007fffffff8ba0) at smt_solver.cpp:200:30
    frame #15: 0x00000000012e06db z3`solver_na2as::check_sat_cc(this=0x000000000251b868, assumptions=0x000000000251d710, clauses=0x00007fffffff8ba0) at solver_na2as.cpp:73:12
    frame #16: 0x00000000012e3345 z3`pool_solver::check_sat_cc_core(this=0x000000000251d6d8, cube=0x000000000251d710, clauses=0x00007fffffff8ba0) at solver_pool.cpp:191:29
    frame #17: 0x00000000012e06db z3`solver_na2as::check_sat_cc(this=0x000000000251d6d8, assumptions=0x00000000025e2b70, clauses=0x00007fffffff8ba0) at solver_na2as.cpp:73:12
    frame #18: 0x000000000210d440 z3`spacer::iuc_solver::check_sat_cc(this=0x00000000025e2ac8, cube=0x00007fffffff8bd0, clauses=0x00007fffffff8ba0) at spacer_iuc_solver.cpp:137:37
    frame #19: 0x00000000020b0c46 z3`spacer::prop_solver::maxsmt(this=0x00000000025149c8, hard=0x00007fffffff8bd0, soft=0x00007fffffff8e20, clauses=0x00007fffffff8ba0) at spacer_prop_solver.cpp:242:24
    frame #20: 0x00000000020b1176 z3`spacer::prop_solver::internal_check_assumptions(this=0x00000000025149c8, hard_atoms=0x00007fffffff8bd0, soft_atoms=0x00007fffffff8e20, clauses=0x00007fffffff8ba0) at spacer_prop_solver.cpp:308:20
    frame #21: 0x00000000020b1a82 z3`spacer::prop_solver::check_assumptions(this=0x00000000025149c8, _hard=0x00007fffffff9228, soft=0x00007fffffff8e20, clause=0x00000000025259b0, num_bg=2, bg=0x00000000026d8cb0, solver_id=1) at spacer_prop_solver.cpp:386:17
    frame #22: 0x000000000206d0fa z3`spacer::pred_transformer::check_inductive(this=0x00000000025258c8, level=0, state=0x00007fffffff9228, uses_level=0x00007fffffff9304, weakness=0) at spacer_context.cpp:1553:27
    frame #23: 0x00000000020a82ab z3`spacer::lemma_bool_inductive_generalizer::operator(this=0x00000000026b8268, lemma=0x00007fffffffa798)(ref<spacer::lemma>&) at spacer_generalizers.cpp:97:16

The behaviour change is random. Sometimes, the behaviour change happens when changing random seeds, sometimes it happens when enabling certain traces.

I have also observed unsoundness in the query right before the query which produces this issue. However, I cannot reproduce unsoundness at the moment.

failed to produce IUC

cmd line args: fp.engine=spacer
commit: 92c15a3
benchmark: https://github.com/zafer-esen/tricera-adt-arr/blob/main/adt-arr/alternating_list-1.i.smt2

Looks like the proof is using an axiom that is assumed inside Spacer. I.e. this proof step is neither a theory hypothesis/axiom nor a part of TR/POB

Spacer assertion violation: File: src/muz/spacer/spacer_context.cpp Line: 950 !lemma->is_ground() || spacer::is_clause(m, l)

instance
commit
The issue is with a bv rewrite rule (file: src/ast/rewriter/bv_rewriter.cpp#L582) that transforms (bvule (+ a b) c) into (and (...)). This rewrite rule is used on a literal (not (bvule ...)) during MBP. This causes our POBs to not be cubes and hence the lemmas to not be clauses.

Segfault inside IUC solver

Spacer segfaults in the following configuration in release mode
fp.spacer.use_sage=false fp.xform.slice=true fp.spacer.global=true fp.spacer.concretize=true fp.spacer.conjecture=true fp.xform.inline_linear=true fp.xform.inline_eager=true fp.xform.tail_simplifier_pve=false fp.engine=spacer fp.print_statistics=true fp.spacer.elim_aux=true fp.spacer.reach_dnf=true fp.spacer.iuc=1 fp.spacer.iuc.arith=1 fp.validate=true fp.spacer.ground_pobs=true fp.spacer.mbqi=false fp.spacer.iuc.print_farkas_stats=false fp.spacer.iuc.old_hyp_reducer=false fp.spacer.ctp=true fp.spacer.native_mbp=true fp.spacer.use_iuc=true fp.spacer.expand_bnd=false
The issue is that the following assertion at spacer_proof_utils.cpp:287 is violated
SASSERT(num_params == parents.size() + 1 /* one param is missing */);
stack trace:
` thread #1, name = 'z3', stop reason = signal SIGSEGV: invalid address (fault address: 0x300000002)

frame #0: 0x00000000013b1a1c z3spacer::mk_fk_from_ab(ast_manager&, ptr_buffer<app, 16u> const&, unsigned int, parameter const*) + 460 frame #1: 0x00000000013b5594 z3spacer::theory_axiom_reducer::reduce(app*) + 7444
frame #2: 0x00000000013a9fc1 z3spacer::iuc_solver::get_iuc(ref_vector<expr, ast_manager>&) + 3873 frame #3: 0x0000000001380eb7 z3spacer::prop_solver::internal_check_assumptions(ref_vector<expr, ast_manager>&, ref_vector<expr, ast_manager>&, vector<ref_vector<expr, ast_manager>, true, unsigned int> const&) + 1431
frame #4: 0x0000000001382949 z3spacer::prop_solver::check_assumptions(ref_vector<expr, ast_manager> const&, ref_vector<expr, ast_manager>&, ref_vector<expr, ast_manager> const&, unsigned int, expr* const*, unsigned int) + 505 frame #5: 0x00000000013528bc z3spacer::pred_transformer::is_reachable(spacer::pob&, ref_vector<expr, ast_manager>, ref, unsigned int&, bool&, datalog::rule const*&, vector<bool, true, unsigned int>&, unsigned int&, bool) + 540
frame #6: 0x0000000001361af2 z3spacer::context::expand_pob(spacer::pob&, sref_buffer<spacer::pob, 16u>&) + 498 frame #7: 0x0000000001363911 z3spacer::context::check_reachability() + 1345
frame #8: 0x0000000001365449 z3spacer::context::solve_core(unsigned int) + 313 frame #9: 0x0000000001365a05 z3spacer::context::solve(unsigned int) + 197
frame #10: 0x000000000136e1f2 z3spacer::dl_interface::query(expr*) + 2818 frame #11: 0x000000000146228f z3horn_tactic::imp::operator()(ref const&, sref_buffer<goal, 16u>&) + 3455
frame Z3Prover#12: 0x00000000009b5e7e z3cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) + 14 frame #13: 0x00000000009be604 z3exec(tactic&, ref const&, sref_buffer<goal, 16u>&) + 52
frame Z3Prover#14: 0x00000000009beba4 z3check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) + 260 frame #15: 0x0000000000ad4aa6 z3(anonymous namespace)::tactic2solver::check_sat_core(unsigned int, expr* const*) + 742
frame Z3Prover#16: 0x0000000000ac6b46 z3solver_na2as::check_sat(unsigned int, expr* const*) + 166 frame #17: 0x0000000000aaaef6 z3combined_solver::check_sat(unsigned int, expr* const*) + 1190
frame Z3Prover#18: 0x0000000000bb7ecd z3cmd_context::check_sat(unsigned int, expr* const*) + 877 frame #19: 0x0000000000bf7dde z3smt2::parser::operator()() + 734
frame Z3Prover#20: 0x0000000000be37e0 z3parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) + 64 frame #21: 0x000000000159bdb6 z3read_smtlib2_commands(char const*) + 534
frame Z3Prover#22: 0x0000000000419212 z3main + 274 frame #23: 0x0000000001684c79 z3__libc_start_main + 777
frame Z3Prover#24: 0x000000000041c2ca z3_start + 42

instance
commit 5f3503c73e9e37ae78d63383bcd063d911b10036

Did not understand some aspects of code

file : merge_generalizer.cpp

function : leq_monotonic_neg_k :
It seems like you are checking the right hand side of the literal alone. I thought you had to check the right hand side of all the lemmas that match the pattern.

function : monotonic_coefficient :
uni_consts is never used
the comment seems to say that A + B >=0 whereas A + B < 0 is being returned.

function : merge_halfspaces :
shouldn't the following this need to be checked ?
fst and scd have no variables on the left hand side.
fst and scd have exactly one variable and no uninterpreted constants on the right hand side

function : leq_monotonic_k :
line: 88 : should this be mk_le instead of mk_eq ?

file : spacer_util.cpp

function : contains_nonlinear :
seems like the whole ast_manager is being copied when calling the function
line 1043 : I think if the expression is var*const, the function will return true, but it should have returned false.

file : spacer_cluster.cpp

function : operator()
I didn't understand what happens when a lemma is close to multiple lemmas ? It seems like the last antiUnifier pattern is stored along with all the previous neighbours ( even those that doesn't match the current pattern ).

   If I understand correctly, the first neighbour of a lemma is the antiunifier pattern and the other neighbours are actual lemmas ?