diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index d4194915b..0107d39a8 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4512,6 +4512,15 @@ namespace smt {
         generate_mutual_exclusion(arrangement_disjunction);
     }
 
+    bool theory_str::get_string_constant_eqc(expr * e, zstring & stringVal) {
+        bool exists;
+        expr * strExpr = get_eqc_value(e, exists);
+        if (!exists) {
+            return false;}
+        u.str.is_string(strExpr, stringVal);
+        return true;
+    }
+    
     /*
      * Look through the equivalence class of n to find a string constant.
      * Return that constant if it is found, and set hasEqcValue to true.
@@ -7019,6 +7028,99 @@ namespace smt {
             set_up_axioms(e);
             propagate();
         }
+
+        // heuristics
+        
+        if (u.str.is_prefix(e)) {
+            check_consistency_prefix(e, is_true);
+        } else if (u.str.is_suffix(e)) {
+            check_consistency_suffix(e, is_true);
+        } else if (u.str.is_contains(e)) {
+            check_consistency_contains(e, is_true);
+        }
+    }
+
+    // terms like int.to.str cannot start with / end with / contain non-digit characters
+    // in the future this could be expanded to regex checks as well
+    void theory_str::check_consistency_prefix(expr * e, bool is_true) {
+        context & ctx = get_context();
+        ast_manager & m = get_manager();
+        expr * needle;
+        expr * haystack;
+
+        u.str.is_prefix(e, needle, haystack);
+        TRACE("str", tout << "check consistency of prefix predicate: " << mk_pp(needle, m) << " prefixof " << mk_pp(haystack, m) << std::endl;);
+        
+        zstring needleStringConstant;
+        if (get_string_constant_eqc(needle, needleStringConstant)) {
+            if (u.str.is_itos(haystack) && is_true) {
+                // needle cannot contain non-digit characters
+                for (unsigned i = 0; i < needleStringConstant.length(); ++i) {
+                    if (! ('0' <= needleStringConstant[i] && needleStringConstant[i] <= '9')) {
+                        TRACE("str", tout << "conflict: needle = \"" << needleStringConstant << "\" contains non-digit character, but is a prefix of int-to-string term" << std::endl;);
+                        expr_ref premise(ctx.mk_eq_atom(needle, mk_string(needleStringConstant)), m);
+                        expr_ref conclusion(m.mk_not(e), m);
+                        expr_ref conflict(rewrite_implication(premise, conclusion), m);
+                        assert_axiom_rw(conflict);
+                        return;
+                    }
+                }
+            }
+        }
+    }
+
+    void theory_str::check_consistency_suffix(expr * e, bool is_true) {
+        context & ctx = get_context();
+        ast_manager & m = get_manager();
+        expr * needle;
+        expr * haystack;
+
+        u.str.is_suffix(e, needle, haystack);
+        TRACE("str", tout << "check consistency of suffix predicate: " << mk_pp(needle, m) << " suffixof " << mk_pp(haystack, m) << std::endl;);
+        
+        zstring needleStringConstant;
+        if (get_string_constant_eqc(needle, needleStringConstant)) {
+            if (u.str.is_itos(haystack) && is_true) {
+                // needle cannot contain non-digit characters
+                for (unsigned i = 0; i < needleStringConstant.length(); ++i) {
+                    if (! ('0' <= needleStringConstant[i] && needleStringConstant[i] <= '9')) {
+                        TRACE("str", tout << "conflict: needle = \"" << needleStringConstant << "\" contains non-digit character, but is a suffix of int-to-string term" << std::endl;);
+                        expr_ref premise(ctx.mk_eq_atom(needle, mk_string(needleStringConstant)), m);
+                        expr_ref conclusion(m.mk_not(e), m);
+                        expr_ref conflict(rewrite_implication(premise, conclusion), m);
+                        assert_axiom_rw(conflict);
+                        return;
+                    }
+                }
+            }
+        }
+    }
+
+    void theory_str::check_consistency_contains(expr * e, bool is_true) {
+        context & ctx = get_context();
+        ast_manager & m = get_manager();
+        expr * needle;
+        expr * haystack;
+
+        u.str.is_contains(e, haystack, needle); // first string contains second one
+        TRACE("str", tout << "check consistency of contains predicate: " << mk_pp(haystack, m) << " contains " << mk_pp(needle, m) << std::endl;);
+        
+        zstring needleStringConstant;
+        if (get_string_constant_eqc(needle, needleStringConstant)) {
+            if (u.str.is_itos(haystack) && is_true) {
+                // needle cannot contain non-digit characters
+                for (unsigned i = 0; i < needleStringConstant.length(); ++i) {
+                    if (! ('0' <= needleStringConstant[i] && needleStringConstant[i] <= '9')) {
+                        TRACE("str", tout << "conflict: needle = \"" << needleStringConstant << "\" contains non-digit character, but int-to-string term contains it" << std::endl;);
+                        expr_ref premise(ctx.mk_eq_atom(needle, mk_string(needleStringConstant)), m);
+                        expr_ref conclusion(m.mk_not(e), m);
+                        expr_ref conflict(rewrite_implication(premise, conclusion), m);
+                        assert_axiom_rw(conflict);
+                        return;
+                    }
+                }
+            }
+        }
     }
 
     void theory_str::push_scope_eh() {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 34f371219..bccef5cac 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -645,6 +645,7 @@ protected:
 
     app * mk_value_helper(app * n);
     expr * get_eqc_value(expr * n, bool & hasEqcValue);
+    bool get_string_constant_eqc(expr * n, zstring & stringVal);
     expr * z3str2_get_eqc_value(expr * n , bool & hasEqcValue);
     bool in_same_eqc(expr * n1, expr * n2);
     expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet);
@@ -720,6 +721,10 @@ protected:
     bool new_eq_check(expr * lhs, expr * rhs);
     void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts);
 
+    void check_consistency_prefix(expr * e, bool is_true);
+    void check_consistency_suffix(expr * e, bool is_true);
+    void check_consistency_contains(expr * e, bool is_true);
+
     int ctx_dep_analysis(std::map<expr*, int> & strVarMap, std::map<expr*, int> & freeVarMap,
             std::map<expr*, std::set<expr*> > & unrollGroupMap, std::map<expr*, std::map<expr*, int> > & var_eq_concat_map);
     void trace_ctx_dep(std::ofstream & tout,