mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

moving out construction of expr_ref

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-16 09:29:26 -07:00
parent a93f1f88cc
commit 5f9891c235
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/normal_forms/nnf.cpp
View file

@ -225,8 +225,6 @@ struct nnf::imp {
m_cache_result(other.m_cache_result), m_cache_result(other.m_cache_result),
m_spos(other.m_spos) { m_spos(other.m_spos) {
} }
//frame():m_curr(*(ast_manager*)(nullptr)) {
//}
}; };
// There are four caches: // There are four caches:
@ -335,7 +333,8 @@ struct nnf::imp {
} }
void push_frame(expr * t, bool pol, bool in_q, bool cache_res) { void push_frame(expr * t, bool pol, bool in_q, bool cache_res) {
m_frame_stack.push_back(frame(expr_ref(t, m()), pol, in_q, cache_res, m_result_stack.size())); expr_ref tt(t, m());
m_frame_stack.push_back(frame(tt, pol, in_q, cache_res, m_result_stack.size()));
} }
static unsigned get_cache_idx(bool pol, bool in_q) { static unsigned get_cache_idx(bool pol, bool in_q) {