summaryrefslogtreecommitdiff
path: root/src/theory/strings/infer_info.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/infer_info.cpp')
-rw-r--r--src/theory/strings/infer_info.cpp6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index c75e03440..174bbe2b7 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -95,7 +95,7 @@ std::ostream& operator<<(std::ostream& out, Inference i)
return out;
}
-InferInfo::InferInfo() : d_id(Inference::NONE) {}
+InferInfo::InferInfo() : d_id(Inference::NONE), d_idRev(false) {}
bool InferInfo::isTrivial() const
{
@@ -119,6 +119,10 @@ bool InferInfo::isFact() const
std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
{
out << "(infer " << ii.d_id << " " << ii.d_conc;
+ if (ii.d_idRev)
+ {
+ out << " :rev";
+ }
if (!ii.d_ant.empty())
{
out << " :ant (" << ii.d_ant << ")";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback