summaryrefslogtreecommitdiff
path: root/src/theory/output_channel.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r--src/theory/output_channel.h5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index ad558e115..efd2911ef 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -58,8 +58,9 @@ public:
* Indicate a theory conflict has arisen.
*
* @param n - a conflict at the current decision level. This should
- * be an OR-kinded node of literals that are false in the current
- * assignment.
+ * be an AND-kinded node of literals that are TRUE in the current
+ * assignment and are in conflict (i.e., at least one must be
+ * assigned false).
*
* @param safe - whether it is safe to be interrupted
*/
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback