From bc723fbe89a1fe4d41d7257002a586335683dc46 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 6 Sep 2019 15:07:43 +0300
Subject: [PATCH] fix #2539

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/nlsat/nlsat_solver.cpp       | 1 -
 src/parsers/smt2/smt2scanner.cpp | 2 +-
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index cff7c1e23..0193a0f4d 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -501,7 +501,6 @@ namespace nlsat {
         }
 
         void del(bool_var b) {
-            TRACE("nlsat", tout << "del " << b << "\n";);
             SASSERT(m_bwatches[b].empty());
             //SASSERT(m_bvalues[b] == l_undef);
             m_num_bool_vars--;
diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp
index 5d4c6c472..a4836fe22 100644
--- a/src/parsers/smt2/smt2scanner.cpp
+++ b/src/parsers/smt2/smt2scanner.cpp
@@ -260,7 +260,7 @@ namespace smt2 {
                 throw scanner_exception("invalid empty bit-vector literal", m_line, m_spos);
             return BV_TOKEN;
         }
-        else if ('|') {
+        else if (c == '|') {
             read_multiline_comment();
             return NULL_TOKEN;
         }