Opened 2 weeks ago

Last modified 11 days ago

#49 assigned defect

Build system should check for minimal version of Z3

Reported by: adamatousek Owned by: Henrich Lauko
Priority: minor Milestone: 4.3
Component: other Keywords: build
Cc:

Description

DIVINE build currently fails on Debian with downstream Z3 installed.

Debian provides libz3-dev version 4.4.1-0.4, which seems to be too old to be used by DIVINE, yet the build system attempts to use it:

$ make
...
## Build options: OPT_SIM OPT_Z3 OPT_STP
...
../divine/smt/builder-z3.cpp:82:23: error: no member named 'zext' in namespace 'z3'
                ? z3::zext( arg, bw - childbw )
                  ~~~~^
../divine/smt/builder-z3.cpp:87:23: error: no member named 'sext' in namespace 'z3'
                ? z3::sext( arg, bw - childbw )
                  ~~~~^
...

Change History (1)

comment:1 Changed 11 days ago by mornfall

Milestone: 4.3
Owner: changed from mornfall to Henrich Lauko
Status: newassigned
Note: See TracTickets for help on using tickets.