diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp
index 729475f5c..18d40d48f 100644
--- a/src/parsers/smt2/smt2scanner.cpp
+++ b/src/parsers/smt2/smt2scanner.cpp
@@ -92,7 +92,7 @@ namespace smt2 {
     scanner::token scanner::read_symbol_core() {
         while (true) {
             char c = curr();
-            char n = m_normalized[static_cast<unsigned char>(c)];
+            signed char n = m_normalized[static_cast<unsigned char>(c)];
             if (n == 'a' || n == '0' || n == '-') {
                 m_string.push_back(c);
                 next();
@@ -257,7 +257,7 @@ namespace smt2 {
         m_smtlib2_compliant = ctx.params().m_smtlib2_compliant;
 
         for (int i = 0; i < 256; ++i) {
-            m_normalized[i] = (char) i;
+            m_normalized[i] = (signed char) i;
         }
         m_normalized[static_cast<int>('\t')] = ' ';
         m_normalized[static_cast<int>('\r')] = ' ';
diff --git a/src/parsers/smt2/smt2scanner.h b/src/parsers/smt2/smt2scanner.h
index 60726ca63..8313c24df 100644
--- a/src/parsers/smt2/smt2scanner.h
+++ b/src/parsers/smt2/smt2scanner.h
@@ -42,7 +42,7 @@ namespace smt2 {
         rational           m_number;
         unsigned           m_bv_size;
         // end of data
-        char               m_normalized[256];
+        signed char        m_normalized[256];
 #define SCANNER_BUFFER_SIZE 1024
         char               m_buffer[SCANNER_BUFFER_SIZE];
         unsigned           m_bpos;
diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp
index 451577357..679c46720 100644
--- a/src/smt/smt_enode.cpp
+++ b/src/smt/smt_enode.cpp
@@ -216,7 +216,7 @@ namespace smt {
         // m_lbl_hash should be different from -1, if and only if,
         // there is a pattern that contains the enode. So,
         // I use a trail to restore the value of m_lbl_hash to -1.
-        ctx.push_trail(value_trail<context, char>(m_lbl_hash));
+        ctx.push_trail(value_trail<context, signed char>(m_lbl_hash));
         unsigned h = hash_u(get_owner_id());
         m_lbl_hash = h & (APPROX_SET_CAPACITY - 1);
         // propagate modification to the root m_lbls set.
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 3e174a7a7..7c3224882 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -52,11 +52,11 @@ namespace smt {
 #else
     class app2enode_t : public u_map<enode *> {
     public:
-      void setx(unsigned x, enode *val, enode *def){
-	if(val == 0)
-	  erase(x);
-	else
-	  insert(x,val);
+        void setx(unsigned x, enode *val, enode *def){
+            if (val == 0)
+                erase(x);
+            else
+                insert(x,val);
       }
     };
 #endif
@@ -105,7 +105,7 @@ namespace smt {
         enode_vector        m_parents;          //!< Parent enodes of the equivalence class.
         theory_var_list     m_th_var_list;      //!< List of theories that 'care' about this enode.
         trans_justification m_trans;            //!< A justification for the enode being equal to its root.
-        char                m_lbl_hash;         //!< It is different from -1, if enode is used in a pattern
+        signed char         m_lbl_hash;         //!< It is different from -1, if enode is used in a pattern
         approx_set          m_lbls;
         approx_set          m_plbls;
         enode *             m_args[0];          //!< Cached args