mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-18 16:28:56 +00:00
Code Activity

Fix segfault in dioph_eq.cpp by adding bounds check

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-17 00:04:21 +00:00
parent b5202c65c0
commit 522aa69e09
2 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/dioph_eq.cpp
View file

@ -1094,11 +1094,11 @@ namespace lp {
recalculate_entry(ei);
if (m_e_matrix.m_columns.back().size() == 0) {
if (!m_e_matrix.m_columns.empty() && m_e_matrix.m_columns.back().size() == 0) {
m_e_matrix.m_columns.pop_back();
m_var_register.shrink(m_e_matrix.column_count());
}
if (m_l_matrix.m_columns.back().size() == 0)
if (!m_l_matrix.m_columns.empty() && m_l_matrix.m_columns.back().size() == 0)
m_l_matrix.m_columns.pop_back();
}
remove_irrelevant_fresh_defs();

7
test_with_logic.smt2 Normal file
View file

@ -0,0 +1,7 @@
(set-logic UFNIRA)
(declare-const x Bool)
(declare-const x3 Bool)
(declare-const x1 Int)
(declare-fun cd (Int Int) Int)
(assert (forall ((a Int) (b Int) (c Int)) (or (<= a 1) (<= b 1) (exists ((d Int)) (and (ite (ite (<= (to_int (+ 1.0 0.00000001 (* (to_real b) (to_real b) (to_real b)))) (cd 0 0)) true (is_int (+ 1.0 (* 0.00000001 (/ 1.0 1000000000.0)) (* (to_real b) (to_real b) (to_real b))))) (is_int (/ 0.00000001 (+ 1.0 (to_real d)))) (ite (< (abs (to_real b)) 0.00000001) true (ite (<= (abs b) (cd 0 c)) (is_int (/ (+ 0.00000001 (* (to_real x1) (to_real x1) (to_real (to_int (/ 1.0 (to_real b)))))) (+ 1 1.0))) x3))) (ite (ite (<= b (cd 0 0)) (is_int (+ 1.0 (* (/ 1.0 1000000000.0)) (* (to_real a) (to_real a) (to_real a)))) (is_int (+ 1.0 (* 0.00000001 (/ 1.0 1000000000.0)) (* 0.00000001 (to_real x1) (to_real a)) (* (to_real a) (to_real a) (to_real a))))) x (ite (< a 1.0) true (ite (<= b (cd 0 0)) true (is_int (+ 1.0 (* 0.00000001 (/ 1.0 1000000000.0)) (* (to_real (to_int (/ (to_real d) (+ 1.0 1.0)))) (to_real (to_int (/ (to_real x1) (+ 1.0 (to_real a))))) (to_real (to_int (/ (to_real x1) (+ 1.0 (to_real a))))))))))))))))
(check-sat)