summaryrefslogtreecommitdiff
path: root/src/theory/fp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp')
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 0c41e8ff7..ba9823541 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -202,10 +202,10 @@ namespace rewrite {
// Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder
RewriteResponse compactMinMax (TNode node, bool isPreRewrite) {
+#ifdef CVC4_ASSERTIONS
Kind k = node.getKind();
-
Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX));
-
+#endif
if (node[0] == node[1]) {
return RewriteResponse(REWRITE_DONE, node[0]);
} else {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback