mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

distinguish theory_vars in output

Browse source
This commit is contained in:
Jakob Rath 2024-02-01 12:14:14 +01:00
parent 0b5f163ba7
commit cb6fb7b26b
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/polysat/types.h
View file

@ -93,7 +93,7 @@ namespace polysat {
else if (d.is_bool_var())
return out << d.bool_var();
else if (d.is_eq())
return out << "v" << d.eq().first << " == v" << d.eq().second;
return out << "tv" << d.eq().first << " == tv" << d.eq().second;
else if (d.is_offset_claim()) {
auto offs = d.offset();
return out << "v" << offs.v << " == v" << offs.w << " offset " << offs.offset;