From 4be3926daa1420b3d4a646628977f38c0988fc1b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 5 Sep 2015 16:30:58 -0700
Subject: [PATCH] use signed character type declarations for cross platform
 compilation. Fixes issue #210

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/parsers/smt2/smt2scanner.cpp | 2 +-
 src/qe/qe_lite.cpp               | 4 ++--
 src/tactic/arith/fm_tactic.cpp   | 2 +-
 src/util/vector.h                | 1 +
 4 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp
index f653cbb25..729475f5c 100644
--- a/src/parsers/smt2/smt2scanner.cpp
+++ b/src/parsers/smt2/smt2scanner.cpp
@@ -295,7 +295,7 @@ namespace smt2 {
     
     scanner::token scanner::scan() {
         while (true) {
-            char c = curr();
+            signed char c = curr();
             m_pos = m_spos;
             switch (m_normalized[(unsigned char) c]) {
             case ' ':
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 61fb91524..f045e406e 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -1055,7 +1055,7 @@ namespace fm {
         arith_util               m_util;
         constraints              m_constraints;
         expr_ref_vector          m_bvar2expr;
-        char_vector              m_bvar2sign;
+        signed_char_vector       m_bvar2sign;
         obj_map<expr, bvar>      m_expr2bvar;
         char_vector              m_is_int;
         char_vector              m_forbidden;
@@ -2064,7 +2064,7 @@ namespace fm {
                 switch (m_bvar2sign[p]) {
                 case 0:
                     new_lits.push_back(lit);
-                break;
+                    break;
                 case -1:
                     if (!sign(lit))
                         tautology = true;
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index c180029ae..8d7a0eab0 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -382,7 +382,7 @@ class fm_tactic : public tactic {
         arith_util               m_util;
         constraints              m_constraints;
         expr_ref_vector          m_bvar2expr;
-        char_vector              m_bvar2sign;
+        signed_char_vector       m_bvar2sign;
         obj_map<expr, bvar>      m_expr2bvar;
         char_vector              m_is_int;
         char_vector              m_forbidden;
diff --git a/src/util/vector.h b/src/util/vector.h
index 0757be6e2..faab3b86c 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -430,6 +430,7 @@ public:
 typedef svector<int> int_vector;
 typedef svector<unsigned> unsigned_vector;
 typedef svector<char> char_vector;
+typedef svector<signed char> signed_char_vector;
 typedef svector<double> double_vector;
 
 template<typename Hash, typename Vec>