Any unsatisfiable SMT run results in a Z3Exception
Any exploration using the Z3 SMT solver which turns out to be unsatisfiable results in a Z3Exception (Context mismatch) to be thrown in the background.
How to reproduce
After importing the attaches project into the DSE view, one can execute a deployment synthesis selecting the existing constraint set.
(from redmine: issue id 3772, created on 2019-07-12, closed on 2019-09-26)
- Uploads:
- dse_project.af3_23 Minimal AF3 project for testing