search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.22k stars 1.47k forks source link

Z3 does not recognize the QF_DTLIA logic #7258

Closed yoni206 closed 3 months ago

yoni206 commented 3 months ago

Similar to: https://github.com/Z3Prover/z3/issues/4754

from z3 import *
s = SolverFor("QF_DTLIA")
Traceback (most recent call last):
.
.
.
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b"logic 'QF_DTLIA' is not recognized"

tested on version 4.13.0.

NikolajBjorner commented 3 months ago

It doesn't. the alphabet soup of logics is generally not recognized. You can use "ALL".