Question 1: How could I use Z3 Python API in order to add constraints with unique labels? I was trying something like:
... self.solver.add(self.vm[i] >= 0, 'labelIdx'+str(self.idx)) ...
where self.idx is an integer number which increases for each i, but I get:
z3.z3types.Z3Exception: True, False or Z3 Boolean expression expected. Received labelIdx0
Which means that the arguments of add can not be Strings.
Question 2: Function unsat_core() works only with Solver() objects or also with Optimize() ones. Should I set some option before adding the constraints. Apparently, here [1] this is the procedure.
Thanks!
For tracking unsat cores, you need to use assert_and_track, see here: https://z3prover.github.io/api/html/classz3py_1_1_solver.html#ad1255f8f9ba8926bb04e1e2ab38c8c15
Optimization and unsat-cores do not work together unfortunately. This was recently raised as an issue, see here: https://github.com/Z3Prover/z3/issues/1577. As I understand it, it is not because it cannot be supported, but rather they haven't implemented it yet. Commenting on that ticket can motivate them to add support!