summaryrefslogtreecommitdiff
path: root/src/theory/theory_model_builder.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_model_builder.h')
-rw-r--r--src/theory/theory_model_builder.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index c24d50cbf..bb74569b7 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -58,7 +58,8 @@ class TheoryEngineModelBuilder : public ModelBuilder
* (4) assign constants to all equivalence classes
* of m's equality engine, through alternating
* iterations of evaluation and enumeration,
- * (5) builder-specific post-processing.
+ * (5) builder-specific processing, which includes assigning total
+ * interpretations to uninterpreted functions.
*
* This function returns false if any of the above
* steps results in a lemma sent on an output channel.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback