1

I have problems setting a timeout for my solver:

s = Solver()
encoding = parse_smt2_file("ex.smt2")
s.add(encoding)

s.set("timeout", 600)
solution = s.check()

but I get the following error

Traceback (most recent call last): 
File "/Users/X/Documents/encode.py", line 145, in parse_polyedra("file") 
File "/Users/X/Documents/encode.py", line 108, in parse_polyedra s.set("timeout",1) File "/Users/X/z3/build/z3.py", line 5765, in set Z3_solver_set_params(self.ctx.ref(), self.solver, p.params) 
File "/Users/X/z3/build/z3core.py", line 3969, in Z3_solver_set_params raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) 
Z3Exception: unknown parameter 'timeout'

A list of legal parameters appears, but timeout is not part of it. I took a look to this post, but the problem is not the same. As far as I understand, the parameter should be accepted, it is just that in the stable version the timeout may never happens, but there should not be problems to compile.

Anyway I installed the unstable branch and the problem persist.

Community
  • 1
  • 1
Hernan Ponce de Leon
  • 71
  • 1
  • 4
  • 1
    Could you try the "soft_timeout" option? The plan is to rename this option to just "timeout", but this hasn't been done yet as there may be clashes/inconsistencies with other options. – Christoph Wintersteiger Feb 26 '15 at 16:30

1 Answers1

2

I was able to use the timeout option (and it actually timeouts, and returns the best known solution in the case of optimization) with the following versions:

Python 2.7.9 (default, Mar  1 2015, 12:57:24) 
[GCC 4.9.2] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> import z3
>>> s = z3.Solver()
>>> s.set("timeout", 600)
>>> z3.get_version_string()
'4.4.2'
Emilien
  • 2,385
  • 16
  • 24
  • According to https://stackoverflow.com/questions/60841582/timeout-for-z3-optimize, you can't get the best-known solution when timeout. – Yi Zhao Dec 06 '21 at 11:54