From b14364a11759d563edd104922b7d38ccb22f20aa Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 5 Jul 2017 11:06:40 -0400
Subject: [PATCH] fix theory_str warnings: rename get_value() to
 get_arith_value()

---
 src/smt/theory_str.cpp | 15 ++++++++-------
 src/smt/theory_str.h   |  4 ++--
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 5d46b5349..2e928af37 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1984,7 +1984,8 @@ namespace smt {
         return NULL;
     }
 
-    static inline std::string rational_to_string_if_exists(const rational & x, bool x_exists) {
+    // trace code helper
+    inline std::string rational_to_string_if_exists(const rational & x, bool x_exists) {
         if (x_exists) {
             return x.to_string();
         } else {
@@ -4651,7 +4652,7 @@ namespace smt {
         }
     }
 
-    bool theory_str::get_value(expr* e, rational& val) const {
+    bool theory_str::get_arith_value(expr* e, rational& val) const {
         if (opt_DisableIntegerTheoryIntegration) {
             TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;);
             return false;
@@ -4780,7 +4781,7 @@ namespace smt {
                         }
                     });
 
-                if (ctx.e_internalized(len) && get_value(len, val1)) {
+                if (ctx.e_internalized(len) && get_arith_value(len, val1)) {
                     val += val1;
                     TRACE("str", tout << "integer theory: subexpression " << mk_ismt2_pp(len, m) << " has length " << val1 << std::endl;);
                 }
@@ -8439,7 +8440,7 @@ namespace smt {
 
         // check integer theory
         rational Ival;
-        bool Ival_exists = get_value(a, Ival);
+        bool Ival_exists = get_arith_value(a, Ival);
         if (Ival_exists) {
             TRACE("str", tout << "integer theory assigns " << mk_pp(a, m) << " = " << Ival.to_string() << std::endl;);
             // if that value is not -1, we can assert (str.to-int S) = Ival --> S = "Ival"
@@ -8610,7 +8611,7 @@ namespace smt {
             rational lenValue;
             expr_ref concatlenExpr (mk_strlen(concat), m) ;
             bool allLeafResolved = true;
-            if (! get_value(concatlenExpr, lenValue)) {
+            if (! get_arith_value(concatlenExpr, lenValue)) {
                 // the length fo concat is unresolved yet
                 if (get_len_value(concat, lenValue)) {
                     // but all leaf nodes have length information
@@ -8647,7 +8648,7 @@ namespace smt {
                 expr * var = *it;
                 rational lenValue;
                 expr_ref varlen (mk_strlen(var), m) ;
-                if (! get_value(varlen, lenValue)) {
+                if (! get_arith_value(varlen, lenValue)) {
                     if (propagate_length_within_eqc(var)) {
                         axiomAdded = true;
                     }
@@ -9479,7 +9480,7 @@ namespace smt {
                   bool unrLenValue_exists = get_len_value(unrFunc, unrLenValue);
                   tout << "unroll length: " << (unrLenValue_exists ? unrLenValue.to_string() : "?") << std::endl;
                   rational cntInUnrValue;
-                  bool cntHasValue = get_value(cntInUnr, cntInUnrValue);
+                  bool cntHasValue = get_arith_value(cntInUnr, cntInUnrValue);
                   tout << "unroll count: " << (cntHasValue ? cntInUnrValue.to_string() : "?")
                   << " low = "
                   << (low_exists ? low.to_string() : "?")
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 0bbc44ab8..7f39efa70 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -219,7 +219,7 @@ protected:
     /*
      * If DisableIntegerTheoryIntegration is set to true,
      * ALL calls to the integer theory integration methods
-     * (get_value, get_len_value, lower_bound, upper_bound)
+     * (get_arith_value, get_len_value, lower_bound, upper_bound)
      * will ignore what the arithmetic solver believes about length terms,
      * and will return no information.
      *
@@ -464,7 +464,7 @@ protected:
     bool in_same_eqc(expr * n1, expr * n2);
     expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet);
 
-    bool get_value(expr* e, rational& val) const;
+    bool get_arith_value(expr* e, rational& val) const;
     bool get_len_value(expr* e, rational& val);
     bool lower_bound(expr* _e, rational& lo);
     bool upper_bound(expr* _e, rational& hi);