From 1aae53f48c9d82fa3173f9a33054e8d7b5896830 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 28 Dec 2014 15:26:41 +0000 Subject: [PATCH] FPA: comment fixes Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 846d6ddb7..bfc038cf7 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -846,11 +846,11 @@ bool float_decl_plugin::is_unique_value(app* e) const { case OP_FLOAT_RM_TOWARD_ZERO: return true; case OP_FLOAT_PLUS_INF: /* No; +oo == fp(#b0 #b11 #b00) */ - case OP_FLOAT_MINUS_INF: /* Nol -oo == fp #b1 #b11 #b00) */ + case OP_FLOAT_MINUS_INF: /* No; -oo == fp #b1 #b11 #b00) */ case OP_FLOAT_PLUS_ZERO: /* No; +zero == fp #b0 #b00 #b000) */ case OP_FLOAT_MINUS_ZERO: /* No; -zero == fp #b1 #b00 #b000) */ case OP_FLOAT_NAN: /* No; NaN == (fp #b0 #b111111 #b0000001) */ - case OP_FLOAT_VALUE: /* above */ + case OP_FLOAT_VALUE: /* see NaN */ return false; case OP_FLOAT_FP: return m_manager->is_unique_value(e->get_arg(0)) &&