From 55ea1929e922f0999c89bc7d13978461ab0ec412 Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Mon, 11 May 2026 19:22:45 +0200 Subject: [PATCH] A bit more "dot" improvements --- src/smt/seq/seq_nielsen_pp.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/smt/seq/seq_nielsen_pp.cpp b/src/smt/seq/seq_nielsen_pp.cpp index 8c7127674..f4faa67ea 100644 --- a/src/smt/seq/seq_nielsen_pp.cpp +++ b/src/smt/seq/seq_nielsen_pp.cpp @@ -147,6 +147,18 @@ namespace seq { } app* a = to_app(e); expr* x, * y; + if (m.is_or(e)) { + app* ap = to_app(e); + std::string res; + res = arith_expr_html(ap->get_arg(0), names, next_id, m); + for (unsigned i = 1; i < ap->get_num_args(); ++i) { + res += " || "; + res += arith_expr_html(ap->get_arg(i), names, next_id, m); + } + return res; + } + if (m.is_not(e, x)) + return "!(" + arith_expr_html(x, names, next_id, m) + ")"; if (arith.is_le(e, x, y)) { return arith_expr_html(x, names, next_id, m) + " < " + arith_expr_html(y, names, next_id, m); } @@ -521,8 +533,8 @@ namespace seq { int_constraints[++prev] = int_constraints[i]; } int_constraints.resize(prev); - out << "Int:
"; if (!any) { out << "Cnstr:
"; any = true; } + out << "Int:
"; for (const auto& s : int_constraints) { out << s << "
"; }