mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

print column value

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-02-20 09:55:33 -08:00
parent f50f21198e
commit fbfbfa5d76
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -254,7 +254,7 @@ namespace lp {
out << "bounds:\n"; out << "bounds:\n";
for (unsigned v = 0; v < m_var_register.size(); ++v) { for (unsigned v = 0; v < m_var_register.size(); ++v) {
unsigned j = m_var_register.local_to_external(v); unsigned j = m_var_register.local_to_external(v);
out << "j" << j << ": "; out << "j" << j << ":= " << lra.get_column_value(j) << ": ";
if (lra.column_has_lower_bound(j)) if (lra.column_has_lower_bound(j))
out << lra.column_lower_bound(j).x << " <= "; out << lra.column_lower_bound(j).x << " <= ";
out << "x" << v; out << "x" << v;