diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index e4394e9b2..f561f82d7 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -6495,7 +6495,7 @@ class Optimize(Z3PPObject):
         return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
 
     def reason_unknown(self):
-	"""Return a string that describes why the last `check()` returned `unknown`."""
+        """Return a string that describes why the last `check()` returned `unknown`."""
         return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
 
     def model(self):
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index fb20a81c6..231b73fe3 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -157,7 +157,7 @@ namespace smt {
         u_map<bool_var>             m_expr2bool_var;
 #endif
         ptr_vector<expr>            m_bool_var2expr;         // bool_var -> expr
-        char_vector                 m_assignment;  //!< mapping literal id -> assignment lbool
+        signed_char_vector          m_assignment;  //!< mapping literal id -> assignment lbool
         vector<watch_list>          m_watches;     //!< per literal
         vector<clause_set>          m_lit_occs;    //!< index for backward subsumption
         svector<bool_var_data>      m_bdata;       //!< mapping bool_var -> data