From 52fdb4d291e38eb5601dac08125309fc79c03210 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 26 May 2020 10:56:10 -0700 Subject: [PATCH] fix issue https://github.com/Z3Prover/z3/issues/4438 Signed-off-by: Lev Nachmanson --- src/smt/theory_arith_nl.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 653e4d325..d75ab0f13 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -96,7 +96,7 @@ void theory_arith::mark_dependents(theory_var v, svector & vars // If s is a base variable different from v and it is free, then this row can be ignored. // It doesn't need to be part of the non linear cluster. For all purposes, this variable // was eliminated by substitution. - if (is_free(s) && s != v) + if (s != null_theory_var && is_free(s) && s != v) continue; typename vector::const_iterator it2 = r.begin_entries(); typename vector::const_iterator end2 = r.end_entries();