From 31d44471a19be4b64cd9d3da3225f3bab72bd79f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 14 Aug 2018 13:52:29 +0800
Subject: [PATCH] remove some warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp        | 1 +
 src/util/lp/lar_constraints.h | 1 +
 src/util/lp/nra_solver.cpp    | 2 ++
 src/util/lp/ul_pair.h         | 1 +
 4 files changed, 5 insertions(+)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 0fbc3d119..303526fcc 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -395,6 +395,7 @@ class theory_lra::imp {
     void ensure_nra() {
         if (!m_nra) {
             m_nra = alloc(nra::solver, *m_solver.get(), m.limit(), ctx().get_params());
+            m_switcher.m_nra = &m_nra;
             for (auto const& _s : m_scopes) {
                 (void)_s;
                 m_nra->push();
diff --git a/src/util/lp/lar_constraints.h b/src/util/lp/lar_constraints.h
index 6305089b4..e4b8cbf41 100644
--- a/src/util/lp/lar_constraints.h
+++ b/src/util/lp/lar_constraints.h
@@ -39,6 +39,7 @@ inline std::string lconstraint_kind_string(lconstraint_kind t) {
     case GE: return std::string(">=");
     case GT: return std::string(">");
     case EQ: return std::string("=");
+    case NE: return std::string("!=");
     }
     lp_unreachable();
     return std::string(); // it is unreachable
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index ce334b3fc..4bcea04c1 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -190,6 +190,8 @@ namespace nra {
             case lp::lconstraint_kind::EQ:
                 lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);                
                 break;
+            default:
+                lp_assert(false); // unreachable
             }
             m_nlsat->mk_clause(1, &lit, a);
         }               
diff --git a/src/util/lp/ul_pair.h b/src/util/lp/ul_pair.h
index e4fbd47e5..e7ac68ed2 100644
--- a/src/util/lp/ul_pair.h
+++ b/src/util/lp/ul_pair.h
@@ -39,6 +39,7 @@ inline std::ostream& operator<<(std::ostream& out, lconstraint_kind k) {
     case GE: return out << ">=";
     case GT: return out << ">";
     case EQ: return out << "=";
+    case NE: return out << "!=";
     }
     return out << "??";
 }