Page MenuHomeIsabelle/Phabricator
Create Task
Maniphest T29

Update component for Z3
Open, NormalPublic
Actions

Description

Follow recent development / stable release of the important Z3 project, with current multi-platform support.

This probably requires significant changes of the Isabelle/SMT setup.

Event Timeline

makarius triaged this task as High priority.Oct 29 2020, 2:43 PM
makarius created this task.

Not yet for the Isabelle2021 release, unless someone does it very quickly and thoroughly during 01-Nov-2020..15-Dec-2020.

makarius lowered the priority of this task from High to Normal.Oct 29 2020, 2:45 PM
makarius added a project: provers.Oct 29 2020, 5:17 PM
mathias.fleury added a subscriber: mathias.fleury.EditedMar 17 2021, 6:28 PM

Basically currently the proof format of Z3 has bugs that we cannot solve on the Isabelle side (https://github.com/Z3Prover/z3/issues/5073). Fixing those requires either internal Z3 knowledge or time from a Z3 developer.

Additionally, Nikolaj Bjorner is reworking the proof format. Currently it looks like a lot more work on the Isabelle side (trimming the proof). Also handling of inprocessing is not clear yet.