mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-20 23:44:41 +00:00
Code Activity

Update nlsat_explain.cpp

Browse source 
Remove a duplicate call
This commit is contained in:
Lev Nachmanson 2025-12-16 17:55:26 -10:00 • committed by GitHub
parent a6f44f8c88
commit 543a473993
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/nlsat_explain.cpp
View file

@ -457,8 +457,7 @@ namespace nlsat {
TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";);
insert_fresh_factors_in_todo(lc);
if (!is_zero(lc) && sign(lc)) {
insert_fresh_factors_in_todo(lc);
TRACE(nlsat_explain, tout << "lc does no vaninsh\n";);
TRACE(nlsat_explain, tout << "lc does no vanish\n";);
return;
}
add_zero_assumption(lc);