3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-13 14:49:27 -07:00
parent 9f42338de8
commit 9223f611ba

View file

@ -814,6 +814,8 @@ theory_var theory_diff_logic<Ext>::mk_var(enode* n) {
template<typename Ext>
void theory_diff_logic<Ext>::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");