Fix generation of unsat cores
Z3 supports the generation of unsat cores that provide guidance which constraints cause an SMT problem to be unsatisfiable.
Steps to reproduce:
- load the ACC model
- import it into the DSE perspective
- Define two obviously contradicting "Allocation" constraints where the same Task should be allocated to different ECUs.
- Start a Deployment synthesis whose result therefore consequently "unsatisfiable".
Expected result: contradicting constraints should be highlighted in the DSE navigator and printed on the Eclipse console. Actual result: Unsat core generation seems to fail and therefore none of the above can be observed.
See ACC.af3_23
Edited by Simon Barner