Model Graph

Formula Input

Input

Formula∃x. W(x,x) ∧ f(b) = x

Eager Evaluation

Formula Tree

∃x

∧

W

x

x

=

f()

b

x

Model Checker

∃x. W(x,x) ∧ f(b) = x

W(1,1) ∧ f(b) = 1

W(1,1)

f(b) = 1