mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

remove assert #7032

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-02 14:12:41 -08:00
parent 331507c4cd
commit 585d027668
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/lar_solver.cpp
View file

@ -1158,7 +1158,6 @@ namespace lp {
if (!v.y.is_zero()) { if (!v.y.is_zero()) {
v = impq(v.x + delta * v.y); v = impq(v.x + delta * v.y);
TRACE("lar_solver_feas", tout << "x[" << j << "] = " << v << "\n";); TRACE("lar_solver_feas", tout << "x[" << j << "] = " << v << "\n";);
SASSERT(!column_is_int(j) || v.is_int());
} }
} }
} }