diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-31 14:39:29 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-31 14:39:29 -0700 |
| commit | e5992fc62ac04a7dff4165c2e54282ac06bd7283 (patch) | |
| tree | 2626b98ecbe62fc82e01fcc7983c1919d25efdf3 /src/theory/uf | |
| parent | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (diff) | |
Fix Unimplemented() macros missed in #3366. (#3424)
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index bb1e434f2..98e330df4 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1684,12 +1684,12 @@ void CardinalityExtension::preRegisterTerm(TNode n) Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier"; Debug("uf-ss-na") << " (" << f << ")"; Debug("uf-ss-na") << std::endl; - Unimplemented("Cannot perform finite model finding on arithmetic quantifier"); + Unimplemented() << "Cannot perform finite model finding on arithmetic quantifier"; }else if( tn.isDatatype() ){ Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier"; Debug("uf-ss-na") << " (" << f << ")"; Debug("uf-ss-na") << std::endl; - Unimplemented("Cannot perform finite model finding on datatype quantifier"); + Unimplemented() << "Cannot perform finite model finding on datatype quantifier"; } */ } |