From cb6fb7b26baf6c168b6de733b18cd77efe39ec06 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 1 Feb 2024 12:14:14 +0100 Subject: [PATCH] distinguish theory_vars in output --- src/sat/smt/polysat/types.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h index 4ccdb8077..af8718523 100644 --- a/src/sat/smt/polysat/types.h +++ b/src/sat/smt/polysat/types.h @@ -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;