Home
last modified time | relevance | path

Searched refs:m_skolemize_decl (Results 1 – 4 of 4) sorted by relevance

/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/
H A Dast.cpp741 m_skolemize_decl(nullptr), in basic_decl_plugin()
914 case PR_SKOLEMIZE: return mk_proof_decl("sk", k, 0, m_skolemize_decl); in mk_proof_decl()
1037 DEC_REF(m_skolemize_decl); in finalize()
H A Dast.h1160 func_decl * m_skolemize_decl; variable
/dports/math/z3/z3-z3-4.8.13/src/ast/
H A Dast.cpp849 case PR_SKOLEMIZE: return mk_proof_decl("sk", k, 0, m_skolemize_decl); in mk_proof_decl()
972 DEC_REF(m_skolemize_decl); in finalize()
H A Dast.h1163 func_decl * m_skolemize_decl = nullptr; variable