mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix #2928 - test case is actually abuse of qe2. It is reasonable for qe2 to assume that simplify was applied first

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-03 08:43:45 -08:00
parent 2398834206
commit 18280a9737
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_bv.cpp
View file

@ -161,7 +161,7 @@ namespace smt {
e = ctx.mk_enode(n, !m_params.m_bv_reflect, false, m_params.m_bv_cc); e = ctx.mk_enode(n, !m_params.m_bv_reflect, false, m_params.m_bv_cc);
mk_var(e); mk_var(e);
} }
SASSERT(e->get_th_var(get_id()) != null_theory_var); // SASSERT(e->get_th_var(get_id()) != null_theory_var);
return e; return e;
} }