summaryrefslogtreecommitdiff
path: root/src/theory/sets
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-05-05 09:35:12 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2017-05-05 09:35:31 -0500
commit5ce46e8a6ac10388b7a2032c7d67a81da0edbd5e (patch)
tree4670bd6270c5681b0f5bf7a95b3342f3229ac62d /src/theory/sets
parentb8d1e24fb00ca15dc523ec45d791473c1e5b8756 (diff)
Fix error message.
Diffstat (limited to 'src/theory/sets')
-rw-r--r--src/theory/sets/theory_sets_type_rules.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 7462847b6..b8c0a8055 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -192,7 +192,7 @@ struct UniverseSetTypeRule {
Assert(check);
TypeNode setType = n.getType();
if(!setType.isSet()) {
- throw TypeCheckingExceptionPrivate(n, "COMPLEMENT operates on a set, non-set object found");
+ throw TypeCheckingExceptionPrivate(n, "Non-set type found for universe set");
}
return setType;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback