Open meditans opened 5 years ago
Hi,
I am no expert in the Fixedpoint API, but you may be using the API incorrectly. This error is raised by the Z3 library itself.
Could you try to reproduce this with the C or the Python API? If you can get it to work with one of the official APIs, then I would have strong evidence to believe that the problem may be somewhere in the Haskell bindings.
Hi, I think I am indeed using the haskell api incorrectly! The question was mainly along the lines of "what am I doing wrong?", because my translation seems to me a fairly close analogue of the smt2-lib version. In the meantime, I found your old bitbucket repo, and saw how the fixpoint API was added, and I'd like to ping @DAHeath, which should be more knowledgeable on this aspect.
Hi, I'm trying to translate this example in z3's documentation using the api provided by this package. The closest thing I can get is:
Unfortunately, if I try to run the
run
function, I get, after the warning I inserted:Could you show me how to get the output of the example problem?
NOTE for the reasons outlined in [#9] you shouldn't use the last
z3
(z3-4.7.1
is ok)