mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

fix #2767

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-02 09:15:04 -08:00
parent 17d67c1b50
commit 2bf9b5ca8b
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_dense_diff_logic_def.h
View file

@ -85,6 +85,8 @@ namespace smt {
if (m_params.m_arith_reflect) if (m_params.m_arith_reflect)
internalize_term_core(to_app(to_app(n)->get_arg(0))); internalize_term_core(to_app(to_app(n)->get_arg(0)));
theory_var s = internalize_term_core(to_app(to_app(n)->get_arg(1))); theory_var s = internalize_term_core(to_app(to_app(n)->get_arg(1)));
if (null_theory_var == s)
return s;
enode * e = ctx.mk_enode(n, !m_params.m_arith_reflect, false, true); enode * e = ctx.mk_enode(n, !m_params.m_arith_reflect, false, true);
theory_var v = mk_var(e); theory_var v = mk_var(e);
add_edge(s, v, k, null_literal); add_edge(s, v, k, null_literal);