mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 09:55:19 +00:00
print also column values
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
22cfab3d42
commit
488c74d3cc
|
@ -2520,7 +2520,8 @@ namespace lp {
|
|||
}
|
||||
if (!has_fresh) {
|
||||
for (const auto& p : get_term_from_entry(i)) {
|
||||
out << "\tx" << p.var() << ": " << lra.get_bounds_string(local_to_lar_solver(p.var())) << "\n";
|
||||
auto j = local_to_lar_solver(p.var());
|
||||
out << "\tx" << p.var() << " := " << lra.get_column_value(j) << " " << lra.get_bounds_string(j) << "\n";
|
||||
}
|
||||
} else {
|
||||
out << "\thas fresh vars\n";
|
||||
|
|
Loading…
Reference in a new issue