fix #2539

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Sep 6, 2019 · bc723fb · bc723fb
1 parent 8ec6219
commit bc723fb
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git 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
@@ -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;
         }