summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/theory/strings/normal_form.cpp5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index 249f53bf7..6622afebd 100644
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -205,10 +205,13 @@ uint64_t NormalForm::getComplexity()
}
} while (!visit.empty());
- d_complexity = 0;
+ d_complexity = d_exp.size();
for (const Node& n : d_nf)
{
d_complexity += visited[n];
+ if (!n.isConst()) {
+ d_complexity++;
+ }
}
d_complexityComputed = true;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback