0

I have the following code

s = SolverFor("QF_LIA")
s.set("timeout", 1000)
#added when edited
s.check()

But I'm getting this error:

    s.set("timeout", 1000)

    line 6438, in set
    Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)

    line 3654, in Z3_solver_set_params_elems.Check(a0)

    line 1378, in Check
    raise self.Exception(self.get_error_message(ctx, err))

What am I doing wrong here? thx for the help!

EDIT

I added s.check (), could you check if you get a error with this line of code.

Andre Oliveira
  • 45
  • 6

1 Answers1

0

There is a related post here

The following example works for me without error:

from z3 import *

s = SolverFor("QF_LIA")
s.set("timeout", 1000)

print(z3.get_version_string())

Output:

python.exe -VV
Python 3.7.4 (tags/v3.7.4:e09359112e, Jul  8 2019, 20:34:20) [MSC v.1916 64 bit (AMD64)]

python.exe test.py
4.8.5
Axel Kemper
  • 10,544
  • 2
  • 31
  • 54
  • Hi thx for the help, but i have the same version as you and I get always the same error. Do you know why i get this error? the only thing that it's different is that you are using 64 bits python. – Andre Oliveira Jul 16 '19 at 13:15
  • Could you check if you add s.check() you get a error, please? – Andre Oliveira Jul 16 '19 at 13:45
  • Perhaps you have combined Z3 32-bit binaries with 64-bit Python? That does not work. – Axel Kemper Jul 16 '19 at 15:32
  • in that case, you have the same problem as me... i tried without the s.check() and it worked for me too, but if I add the s.chech() i get that error. Do you know why? – Andre Oliveira Jul 16 '19 at 16:25
  • 1
    `s.check()` does not result in an error in my tests. Something must be wrong with your installation, I'm afraid. – Axel Kemper Jul 17 '19 at 06:59