# Copyright (c) Microsoft Corporation 2015 from __future__ import print_function from z3 import * def visitor(e, seen): if e in seen: return seen[e] = True yield e if is_app(e): for ch in e.children(): for e in visitor(ch, seen): yield e return if is_quantifier(e): for e in visitor(e.body(), seen): yield e return x, y = Ints('x y') fml = x + x + y > 2 seen = {} for e in visitor(fml, seen): if is_const(e) and e.decl().kind() == Z3_OP_UNINTERPRETED: print("Variable", e) else: print(e)