search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

invalid use of indexed identifier, unknown builtin function int2bv #5213

Closed leonardoalt closed 3 years ago

leonardoalt commented 3 years ago

Input: https://gist.github.com/leonardoalt/6f08f54654ed8ebe4620e1b06eed9edc Running z3 a.smt2 gives me

(error "line 42 column 1808: invalid use of indexed identifier, unknown builtin function int2bv")
(error "line 52 column 1833: invalid use of indexed identifier, unknown builtin function int2bv")
sat

I've used int2bv in similar ways before but not in Horn. Is in unknown specifically for the Horn logic? It works fine via the c++ API. Or is my smtlib code wrong?

agurfinkel commented 3 years ago

int2bv and in general mixing LIA and BV in HORN is not supported. It might "not crash" for some instances, but there are not guarantees. I suspect that int2bv is not registered to the list of builtin functions in the theory that Spacer is using. This particular issue could be fixed (perhaps by setting a theory manually, there are options for that), but I do not know what the end-result will be. For instance, things might just work if these operators are only used "locally", and Spacer only needs to determine whether they are satisfiable, and substitute them by values during POB computation.

@NikolajBjorner would know more about when int2bv is registered and when it is not.

You can use fp.spacer.logic to set spacer to some logic string known to Z3.

NikolajBjorner commented 3 years ago

int2bv is not standard SMTLIB so it does not get declared by default. Only in certain logics or when logics are not set. I added declarations of int2bv for the HORN logic. HORN is also not a standard SMTLIB logic.