search

zevv / nimz3

Nim binding for the Z3 theorem prover
25 stars 3 forks source link

hint for solving failure of optimize test? #6

Open pietroppeter opened 2 years ago

pietroppeter commented 2 years ago

the test using optimize api is skipped and mark as "failing with newer versions of z3": https://github.com/zevv/nimz3/blob/master/tests/test1.nim#L204

I was able to reproduce the failure but also a slight change of code (instead of if s.check ..., use a echo s.check()), makes the code run fine. It seems a very weird behavior to me but maybe this can help someone to better understand why the failure.

See also a Nimib document with all examples running: https://pietroppeter.github.io/nblog/drafts/z3_examples.html

zevv commented 2 years ago

Hmm, for me this still results in a segmentation fault in the call to s.check(). I'llleave this ticket open and might pick this up when I find the time and motivation.

Thanks for the report!

pietroppeter commented 2 years ago

for me this still results in a segmentation fault in the call to s.check()

odd but not stranger than the fact that it does not fail for me. maybe z3 version might play a role, I think I was running the latests (I ran their script to build, not sure if it builds the development or latest release).

Anyway z3 is really fun and I am happy I started hacking on it, thanks for making it available for nim!