Cannot enable or use get-unsat-assumptions via Python Z3_eval_smtlib2_string #7445
Closed
Description
Using z3 built from current master abd1674, following the instructions from the README to build and use the Python bindings in a virtualenv, I cannot enable or use get-unsat-assumptions via Z3_eval_smtlib2_string. From the transcript below you can see that:
(set-option :produce-unsat-assumptions true)fails saying it's too late to set it- the above error message is repeated for further commands on that context (minor bug, may be intended behavior?)
- with a fresh context, z3 replies
unsupportedto(get-option :produce-unsat-assumptions)(minor bug) - actually trying to use
get-unsat-assumptionsfails with an error saying to set the option to true (expected given the default is false, but means being unable to set the option is a problem)
Is there another method to set the option to true on the context before sending strings? I can't set it with z3.set_param/set_option.
(venv) [jbosboom@promenade python]$ pwd
/home/jbosboom/github-repos/z3/build/python
(venv) [jbosboom@promenade python]$ python
Python 3.12.7 (main, Oct 1 2024, 11:15:50) [GCC 14.2.1 20240910] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import z3
>>> z3.get_version_string()
'4.13.4'
>>> ctx = z3.Context()
>>> z3.Z3_eval_smtlib2_string(ctx.ref(), '(set-option :produce-unsat-assumptions true)')
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "/home/jbosboom/github-repos/z3/build/python/z3/z3core.py", line 3612, in Z3_eval_smtlib2_string
_elems.Check(a0)
File "/home/jbosboom/github-repos/z3/build/python/z3/z3core.py", line 1566, in Check
raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'(error "line 1 column 40: error setting \':produce-unsat-assumptions\', option value cannot be modified after initialization")\n'
>>> z3.Z3_eval_smtlib2_string(ctx.ref(), '(get-option :produce-unsat-assumptions)')
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "/home/jbosboom/github-repos/z3/build/python/z3/z3core.py", line 3612, in Z3_eval_smtlib2_string
_elems.Check(a0)
File "/home/jbosboom/github-repos/z3/build/python/z3/z3core.py", line 1566, in Check
raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'(error "line 1 column 40: error setting \':produce-unsat-assumptions\', option value cannot be modified after initialization")\n'
>>> ctx = z3.Context()
>>> z3.Z3_eval_smtlib2_string(ctx.ref(), '(get-option :produce-unsat-assumptions)')
'unsupported\n; :produce-unsat-assumptions line: 1 position: 1\n'
>>> ctx = z3.Context()
>>> z3.Z3_eval_smtlib2_string(ctx.ref(), '(declare-const a Bool)(assert a)(check-sat-assuming ((not a)))')
'unsat\n'
>>> z3.Z3_eval_smtlib2_string(ctx.ref(), '(get-unsat-assumptions)')
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "/home/jbosboom/github-repos/z3/build/python/z3/z3core.py", line 3612, in Z3_eval_smtlib2_string
_elems.Check(a0)
File "/home/jbosboom/github-repos/z3/build/python/z3/z3core.py", line 1566, in Check
raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'(error "line 1 column 86: unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)")\n'Metadata
Assignees
Labels
No labels