mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-26 17:02:38 +00:00
Code Activity

Update theory_lra.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-24 14:10:06 -07:00 • committed by GitHub
parent 18b4a86740
commit 538d419978
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_lra.cpp
View file

@ -4287,7 +4287,7 @@ public:
app_ref coeffs2app(u_map<rational> const& coeffs, rational const& offset, bool is_int) {
expr_ref_vector args(m);
for (auto const& [w, coeff] : coeffs) {
expr* o = get_expr(w);
expr_ref o(get_expr(w), m);
// When the overall expression is Real but 'o' is Int (e.g. due to
// to_real(Int) equality constraints in the LP), coerce 'o' to Real
// to avoid sort mismatches when int/real coercions are disabled.