diff options
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_enumerative.cpp')
| -rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 3f6943a72..9d84ea575 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -314,7 +314,9 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) << std::endl; } Assert(terms[i].isNull() - || terms[i].getType().isComparableTo(ftypes[i])); + || terms[i].getType().isComparableTo(ftypes[i])) + << "Incompatible type " << f << ", " << terms[i].getType() + << ", " << ftypes[i] << std::endl; } if (ie->addInstantiation(f, terms)) { |