Closed
Description
Hi, I am new to the pattern feature of z3. I followed the example from here
f = Function('f', IntSort(), IntSort())
g = Function('g', IntSort(), IntSort())
a, b, c = Ints('a b c')
x = Int('x')
s = Solver()
s.set(auto_config=False, mbqi=False)
s.add( ForAll(x, f(g(x)) == x, patterns = [f(g(x))]),
g(a) == c,
g(b) == c,
a != b )
# Display solver state using internal format
print (s.sexpr())
print (s.check())Since it disabled auto_config and mbqi, it is supposed to output unknown since the pattern f(g(x)) doesn't exist. But the result is unsat in my end.
I wonder if there is any other configuration I need to setup for this?
Metadata
Metadata
Assignees
Labels
No labels