mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-10 01:41:57 +00:00
Code Activity

reorder fields, rename overload name clash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-25 16:01:39 -03:00
parent 64f4c9794d
commit 75a40d8f8e
7 changed files with 23 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_seq.cpp
View file

@ -3885,7 +3885,14 @@ std::ostream& theory_seq::display_disequation(std::ostream& out, ne const& e) co
out << "\n";
}
for (unsigned j = 0; j < e.ls().size(); ++j) {
out << e.ls(j) << " != " << e.rs(j) << "\n";
for (expr* t : e.ls(j)) {
out << mk_bounded_pp(t, m) << " ";
}
out << " != ";
for (expr* t : e.rs(j)) {
out << mk_bounded_pp(t, m) << " ";
}
out << "\n";
}
if (e.dep()) {
display_deps(out, e.dep());