diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 2199c46c0..f0692ae57 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -814,6 +814,8 @@ theory_var theory_diff_logic::mk_var(enode* n) { template void theory_diff_logic::set_sort(expr* n) { + if (m_util.is_numeral(n)) + return; if (m_util.is_int(n)) { if (m_lia_or_lra == is_lra) { throw default_exception("difference logic does not work with mixed sorts");