Cannot set pdr_use_farkas option in Z3py

Question

When I try to set the fixedpoint engine to PDR, and I try to set the pdr_use_farkas option, I am getting an unknown_parameter error.

In particular, I am using the following options on the fixedpoint object:

fp.set(engine='1',pdr_use_farkas=True,unbound_compressor=False,compile_with_widening=True)

This causes the error:

z3.types.Z3Exception: "unknown parameter ':pdr-use-farkas'"

Using set_option doesn't help either. I tried

set_option(dl_engine='1')
set_option(dl_pdr_use_farkas=True)

and I'm getting "unknown option".

Where am I making the mistake?

I'm using Z3 4.3.1 64bit.

Answer 1

The parameter names have changed between versions as newer versions include a name-space mechanism for parameter names. The Python API has a method for listing parameter descriptions: For example:

fp = Fixedpoint() 
print fp.param_descrs() 

prints the set of available parameters (permalink: rise4fun.com/Z3Py/r32)