diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index d1ff65e80..adef6a5b0 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -1452,7 +1452,10 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
             }
         }
         std::reverse(exs.c_ptr(), exs.c_ptr() + exs.size());
-        result = m_util.mk_concat(exs.size(), exs.c_ptr());
+        if (exs.size() == 1) 
+            result = exs[0];
+        else
+            result = m_util.mk_concat(exs.size(), exs.c_ptr());
         return BR_REWRITE3;
     } 
 
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index da5bd0e88..ab32b384a 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1893,6 +1893,8 @@ namespace smt2 {
             if (!curr_is_rparen()) {
                 check_int("invalid push command, integer expected");
                 rational n = curr_numeral();
+                if (n.is_neg())
+                    throw parser_exception("invalid push command, value is negative.");
                 if (!n.is_unsigned())
                     throw parser_exception("invalid push command, value is too big to fit in an unsigned machine integer");
                 num = n.get_unsigned();