mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-05 01:45:15 +00:00
Code Activity

add a check in entry_invariant()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-02 10:54:36 -10:00 • committed by Nikolaj Bjorner
parent 51ac976877
commit a49d2b2067
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2239,6 +2239,10 @@ namespace lp {
if (var_is_fresh(p.var())) if (var_is_fresh(p.var()))
continue; continue;
unsigned j = local_to_lar_solver(p.var()); unsigned j = local_to_lar_solver(p.var());
if (j == UINT_MAX) {
TRACE(dio, tout << "(local: " << "x" << p.var() << ") is not registered \nbad entry:"; print_entry(ei, tout) << "\n";);
return false;
}
if (is_fixed(j)) { if (is_fixed(j)) {
TRACE(dio, tout << "x" << j << "(local: " << "x" << p.var() << ") should not be fixed\nbad entry:"; print_entry(ei, tout) << "\n";); TRACE(dio, tout << "x" << j << "(local: " << "x" << p.var() << ") should not be fixed\nbad entry:"; print_entry(ei, tout) << "\n";);
return false; return false;