summaryrefslogtreecommitdiff
path: root/src/theory/inference_id.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/inference_id.h')
-rw-r--r--src/theory/inference_id.h6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 50c063651..70f70e717 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -772,9 +772,11 @@ enum class InferenceId
// f(x1, .., xn) and P is the reduction predicate for f
// (see theory_strings_preprocess).
STRINGS_REDUCTION,
- //-------------------- prefix conflict
- // prefix conflict (coarse-grained)
+ //-------------------- merge conflicts
+ // prefix conflict
STRINGS_PREFIX_CONFLICT,
+ // arithmetic bound conflict
+ STRINGS_ARITH_BOUND_CONFLICT,
//-------------------- other
// a lemma added during term registration for an atomic term
STRINGS_REGISTER_TERM_ATOMIC,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback