Home
last modified time | relevance | path

Searched refs:m_last_assertions (Results 1 – 2 of 2) sorted by relevance

/dports/math/py-z3-solver/z3-z3-4.8.10/src/solver/
H A Dtactic2solver.cpp40 expr_ref_vector m_last_assertions; member in __anonc3a40cc00111::tactic2solver
106 m_last_assertions(m), in tactic2solver()
195 m_last_assertions.reset(); in check_sat_core2()
196 g->get_formulas(m_last_assertions); in check_sat_core2()
289 return m_last_assertions_valid ? m_last_assertions.size() : m_assertions.size(); in get_num_assertions()
293 return m_last_assertions_valid ? m_last_assertions.get(idx) : m_assertions.get(idx); in get_assertion()
/dports/math/z3/z3-z3-4.8.13/src/solver/
H A Dtactic2solver.cpp40 expr_ref_vector m_last_assertions; member in __anonbe2803850111::tactic2solver
110 m_last_assertions(m), in tactic2solver()
199 m_last_assertions.reset(); in check_sat_core2()
200 g->get_formulas(m_last_assertions); in check_sat_core2()
293 return m_last_assertions_valid ? m_last_assertions.size() : m_assertions.size(); in get_num_assertions()
297 return m_last_assertions_valid ? m_last_assertions.get(idx) : m_assertions.get(idx); in get_assertion()