diff --git a/carcara/src/ast/polyeq.rs b/carcara/src/ast/polyeq.rs
index b7f7dce9..2064ae25 100644
--- a/carcara/src/ast/polyeq.rs
+++ b/carcara/src/ast/polyeq.rs
@@ -10,9 +10,15 @@
 use super::{
     AnchorArg, BindingList, Operator, ProofArg, ProofCommand, ProofStep, Rc, Sort, Subproof, Term,
 };
-use crate::utils::HashMapStack;
+use crate::{ast::Constant, utils::HashMapStack};
 use std::time::{Duration, Instant};
 
+#[derive(Debug, Clone)]
+enum Concat {
+    Constant(String),
+    Term(Rc<Term>),
+}
+
 /// A trait that represents objects that can be compared for equality modulo reordering of
 /// equalities or alpha equivalence.
 pub trait Polyeq {
@@ -266,6 +272,138 @@ impl PolyeqComparator {
 
         self.compare_assoc(op, left_tail, right_tail)
     }
+
+    fn remainder(&mut self, a: Vec<Concat>, b: Vec<Concat>) -> (Vec<Concat>, Vec<Concat>) {
+        fn to_concat(args: &[Rc<Term>]) -> Vec<Concat> {
+            args.iter()
+                .map(|arg| match arg.as_ref() {
+                    Term::Const(Constant::String(s)) => Concat::Constant(s.clone()),
+                    _ => Concat::Term(arg.clone()),
+                })
+                .collect()
+        }
+
+        match (a.first(), b.first()) {
+            (None | Some(_), None) | (None, Some(_)) => (a, b),
+            (Some(a_head), Some(b_head)) => match (a_head, b_head) {
+                (Concat::Constant(a_constant), Concat::Constant(b_constant)) => {
+                    let prefix_length = std::cmp::min(a_constant.len(), b_constant.len());
+                    for i in 0..prefix_length {
+                        if a_constant.chars().nth(i).unwrap() != b_constant.chars().nth(i).unwrap()
+                        {
+                            return (a, b);
+                        }
+                    }
+                    let a_const_rem = &a_constant[prefix_length..];
+                    let b_const_rem = &b_constant[prefix_length..];
+                    let mut new_a = a[1..].to_vec();
+                    let mut new_b = b[1..].to_vec();
+                    if !a_const_rem.is_empty() {
+                        new_a.insert(0, Concat::Constant(a_const_rem.to_owned()));
+                    }
+                    if !b_const_rem.is_empty() {
+                        new_b.insert(0, Concat::Constant(b_const_rem.to_owned()));
+                    }
+                    self.remainder(new_a, new_b)
+                }
+                (Concat::Constant(constant), Concat::Term(term)) => match term.as_ref() {
+                    Term::Op(Operator::StrConcat, args) => {
+                        let concat_args: Vec<Concat> = to_concat(args);
+                        let (constant_rem, concat_rem) = self.remainder(a.clone(), concat_args);
+                        let mut new_b = b[1..].to_vec();
+                        for c in concat_rem.iter().rev() {
+                            new_b.insert(0, c.clone());
+                        }
+                        self.remainder(constant_rem, new_b)
+                    }
+                    _ => {
+                        if constant.is_empty() {
+                            return self.remainder(a[1..].to_vec(), b);
+                        }
+                        (a, b)
+                    }
+                },
+                (Concat::Term(term), Concat::Constant(constant)) => match term.as_ref() {
+                    Term::Op(Operator::StrConcat, args) => {
+                        let concat_args: Vec<Concat> = to_concat(args);
+                        let (concat_rem, constant_rem) = self.remainder(concat_args, b.clone());
+                        let mut new_a = a[1..].to_vec();
+                        for c in concat_rem.iter().rev() {
+                            new_a.insert(0, c.clone());
+                        }
+                        self.remainder(new_a, constant_rem)
+                    }
+                    _ => {
+                        if constant.is_empty() {
+                            return self.remainder(a, b[1..].to_vec());
+                        }
+                        (a, b)
+                    }
+                },
+                (Concat::Term(a_term), Concat::Term(b_term)) => {
+                    match (a_term.as_ref(), b_term.as_ref()) {
+                        (
+                            Term::Op(Operator::StrConcat, a_args),
+                            Term::Op(Operator::StrConcat, b_args),
+                        ) => {
+                            let concat_a_args: Vec<Concat> = to_concat(a_args);
+                            let concat_b_args: Vec<Concat> = to_concat(b_args);
+                            let (concat_a_rem, concat_b_rem) =
+                                self.remainder(concat_a_args, concat_b_args);
+                            let mut new_a = a[1..].to_vec();
+                            let mut new_b = b[1..].to_vec();
+                            for c in concat_a_rem.iter().rev() {
+                                new_a.insert(0, c.clone());
+                            }
+                            for c in concat_b_rem.iter().rev() {
+                                new_b.insert(0, c.clone());
+                            }
+                            self.remainder(new_a, new_b)
+                        }
+                        (Term::Op(Operator::StrConcat, a_args), _) => {
+                            if Polyeq::eq(self, &a_args[0], b_term) {
+                                let concat_a_rem: Vec<Concat> = to_concat(&a_args[1..]);
+                                let mut new_a = a[1..].to_vec();
+                                for c in concat_a_rem.iter().rev() {
+                                    new_a.insert(0, c.clone());
+                                }
+                                let new_b = b[1..].to_vec();
+                                self.remainder(new_a, new_b)
+                            } else {
+                                (a, b)
+                            }
+                        }
+                        (_, Term::Op(Operator::StrConcat, b_args)) => {
+                            if Polyeq::eq(self, &b_args[0], a_term) {
+                                let new_a = a[1..].to_vec();
+                                let concat_b_rem: Vec<Concat> = to_concat(&b_args[1..]);
+                                let mut new_b = b[1..].to_vec();
+                                for c in concat_b_rem.iter().rev() {
+                                    new_b.insert(0, c.clone());
+                                }
+                                self.remainder(new_a, new_b)
+                            } else {
+                                (a, b)
+                            }
+                        }
+                        _ => {
+                            if Polyeq::eq(self, a_term, b_term) {
+                                let new_a = a[1..].to_vec();
+                                let new_b = b[1..].to_vec();
+                                self.remainder(new_a, new_b)
+                            } else {
+                                (a, b)
+                            }
+                        }
+                    }
+                }
+            },
+        }
+    }
+
+    fn compare_strings(&mut self, a: Vec<Concat>, b: Vec<Concat>) -> bool {
+        matches!(self.remainder(a, b), (rem_a, rem_b) if rem_a.is_empty() && rem_b.is_empty())
+    }
 }
 
 impl Polyeq for Rc<Term> {
@@ -328,6 +466,46 @@ impl Polyeq for Term {
                     args: args_b,
                 },
             ) => op_a == op_b && op_args_a == op_args_b && Polyeq::eq(comp, args_a, args_b),
+            (Term::Op(Operator::StrConcat, args_a), Term::Op(Operator::StrConcat, args_b)) => {
+                let concat_args_a: Vec<Concat> = args_a
+                    .iter()
+                    .map(|arg| match arg.as_ref() {
+                        Term::Const(Constant::String(s)) => Concat::Constant(s.clone()),
+                        _ => Concat::Term(arg.clone()),
+                    })
+                    .collect();
+                let concat_args_b: Vec<Concat> = args_b
+                    .iter()
+                    .map(|arg| match arg.as_ref() {
+                        Term::Const(Constant::String(s)) => Concat::Constant(s.clone()),
+                        _ => Concat::Term(arg.clone()),
+                    })
+                    .collect();
+                comp.compare_strings(concat_args_a, concat_args_b)
+            }
+            (Term::Op(Operator::StrConcat, args_a), Term::Const(Constant::String(b))) => {
+                let concat_args_a: Vec<Concat> = args_a
+                    .iter()
+                    .map(|arg| match arg.as_ref() {
+                        Term::Const(Constant::String(s)) => Concat::Constant(s.clone()),
+                        _ => Concat::Term(arg.clone()),
+                    })
+                    .collect();
+                let concat_args_b = vec![Concat::Constant(b.clone())];
+                comp.compare_strings(concat_args_a, concat_args_b)
+            }
+            (Term::Const(Constant::String(a)), Term::Op(Operator::StrConcat, args_b)) => {
+                let concat_args_a = vec![Concat::Constant(a.clone())];
+                let concat_args_b: Vec<Concat> = args_b
+                    .iter()
+                    .map(|arg| match arg.as_ref() {
+                        Term::Const(Constant::String(s)) => Concat::Constant(s.clone()),
+                        _ => Concat::Term(arg.clone()),
+                    })
+                    .collect();
+                comp.compare_strings(concat_args_a, concat_args_b)
+            }
+
             (Term::Op(op_a, args_a), Term::Op(op_b, args_b)) => {
                 comp.compare_op(*op_a, args_a, *op_b, args_b)
             }
diff --git a/carcara/src/checker/mod.rs b/carcara/src/checker/mod.rs
index e28b6893..943050d0 100644
--- a/carcara/src/checker/mod.rs
+++ b/carcara/src/checker/mod.rs
@@ -557,6 +557,10 @@ impl<'c> ProofChecker<'c> {
             "concat_lprop_prefix" => strings::concat_lprop_prefix,
             "concat_lprop_suffix" => strings::concat_lprop_suffix,
 
+            "string_decompose" => strings::string_decompose,
+            "string_length_pos" => strings::string_length_pos,
+            "string_length_non_empty" => strings::string_length_non_empty,
+
             // Special rules that always check as valid, and are used to indicate holes in the
             // proof.
             "hole" => |_| Ok(()),
diff --git a/carcara/src/checker/rules/strings.rs b/carcara/src/checker/rules/strings.rs
index eb6cb9e8..ad1879da 100644
--- a/carcara/src/checker/rules/strings.rs
+++ b/carcara/src/checker/rules/strings.rs
@@ -2,7 +2,10 @@ use super::{
     assert_clause_len, assert_eq, assert_num_args, assert_num_premises, assert_polyeq_expected,
     get_premise_term, RuleArgs, RuleResult,
 };
-use crate::{ast::*, checker::error::CheckerError};
+use crate::{
+    ast::*,
+    checker::{error::CheckerError, rules::assert_polyeq},
+};
 use std::{cmp, time::Duration};
 
 /// A function that takes an `Rc<Term>` and returns a vector corresponding to
@@ -726,6 +729,90 @@ pub fn concat_lprop_suffix(
     assert_eq(&expected, &expanded)
 }
 
+pub fn string_decompose(
+    RuleArgs {
+        premises,
+        args,
+        conclusion,
+        pool,
+        polyeq_time,
+        ..
+    }: RuleArgs,
+) -> RuleResult {
+    assert_num_premises(premises, 1)?;
+    assert_num_args(args, 1)?;
+    assert_clause_len(conclusion, 1)?;
+
+    let term = get_premise_term(&premises[0])?;
+    let rev = args[0].as_term()?.as_bool_err()?;
+    let (t, n) = match_term_err!((>= (strlen t) n) = term)?;
+
+    match_term_err!(
+        (and
+            (= t x)
+            (= (strlen y) n)
+        ) = &conclusion[0]
+    )?;
+
+    let w_1 = build_skolem_prefix(pool, t.clone(), n.clone());
+    let w_2 = build_skolem_suffix_rem(pool, t.clone(), n.clone());
+    let len_term = if rev { w_2.clone() } else { w_1.clone() };
+
+    let expanded = build_term!(
+            pool,
+            (and
+                (= {t.clone()} (strconcat {w_1.clone()} {w_2.clone()}))
+                (= (strlen {len_term.clone()}) {n.clone()})
+            )
+    );
+
+    assert_polyeq(&conclusion[0], &expanded, polyeq_time)
+}
+
+pub fn string_length_pos(RuleArgs { args, conclusion, polyeq_time, .. }: RuleArgs) -> RuleResult {
+    assert_num_args(args, 1)?;
+    assert_clause_len(conclusion, 1)?;
+
+    let t = args[0].as_term()?;
+    let (((t_1, _), (t_2, _)), (t_3, _)) = match_term_err!(
+        (or
+            (and
+                (= (strlen t) 0)
+                (= t "")
+            )
+            (> (strlen t) 0)
+        ) = &conclusion[0]
+    )?;
+
+    assert_polyeq(t_1, t, polyeq_time)?;
+    assert_polyeq(t_2, t, polyeq_time)?;
+    assert_polyeq(t_3, t, polyeq_time)?;
+
+    Ok(())
+}
+
+pub fn string_length_non_empty(
+    RuleArgs {
+        premises, conclusion, polyeq_time, ..
+    }: RuleArgs,
+) -> RuleResult {
+    assert_num_premises(premises, 1)?;
+    assert_clause_len(conclusion, 1)?;
+
+    let term = get_premise_term(&premises[0])?;
+    let (t, _) = match_term_err!((not (= t "")) = term)?;
+
+    let (t_conc, _) = match_term_err!(
+        (not
+            (= (strlen t) 0)
+        ) = &conclusion[0]
+    )?;
+
+    assert_polyeq(t_conc, t, polyeq_time)?;
+
+    Ok(())
+}
+
 mod tests {
     #[test]
     fn concat_eq() {
@@ -1192,7 +1279,7 @@ mod tests {
                    (define-fun r_skolem () String (ite (>= (str.len "a") (str.len (str.++ "a" c))) (str.substr "a" (str.len (str.++ "a" c)) (- (str.len "a") (str.len (str.++ "a" c)))) (str.substr (str.++ "a" c) (str.len "a") (- (str.len (str.++ "a" c)) (str.len "a")))))
                    (step t1 (cl (and (or (= "a" (str.++ "a" c r_skolem)) (= (str.++ "a" c) (str.++ "a" r_skolem))) (not (= r_skolem "")) (> (str.len r_skolem) 0))) :rule concat_split_prefix :premises (h1 h2))"#: false,
             }
-            r#"Conclusion term is not of the form (and (or (= x y) (= z w)) (not (= r "")) (> (str.len r) 0))"# {
+            "Conclusion term is not of the form (and (or (= x y) (= z w)) (not (= r \"\")) (> (str.len r) 0))" {
                 r#"(assume h1 (= (str.++ a b c) (str.++ c d e)))
                    (assume h2 (not (= (str.len (str.++ a b)) (str.len c))))
                    (define-fun r_skolem () String (ite (>= (str.len (str.++ a b)) (str.len c)) (str.substr (str.++ a b) (str.len c) (- (str.len (str.++ a b)) (str.len c))) (str.substr c (str.len (str.++ a b)) (- (str.len c) (str.len (str.++ a b))))))
@@ -1277,7 +1364,7 @@ mod tests {
                    (define-fun r_skolem () String (ite (>= (str.len (str.++ "b" b)) (str.len c)) (str.substr (str.++ "b" b) 0 (- (str.len (str.++ "b" b)) (str.len c))) (str.substr c 0 (- (str.len c) (str.len (str.++ "b" b))))))
                    (step t1 (cl (and (or (= (str.++ "b" b) (str.++ r_skolem c)) (= c (str.++ r_skolem (str.++ "b" b)))) (not (= r_skolem "")) (> (str.len r_skolem) 0))) :rule concat_split_suffix :premises (h1 h2))"#: false,
             }
-            r#"Conclusion term is not of the form (and (or (= x y) (= z w)) (not (= r "")) (> (str.len r) 0))"# {
+            "Conclusion term is not of the form (and (or (= x y) (= z w)) (not (= r \"\")) (> (str.len r) 0))" {
                 r#"(assume h1 (= (str.++ a b c d) (str.++ b c d e)))
                    (assume h2 (not (= (str.len (str.++ c d)) (str.len (str.++ c d e)))))
                    (define-fun r_skolem () String (ite (>= (str.len (str.++ c d)) (str.len (str.++ c d e))) (str.substr (str.++ c d) 0 (- (str.len (str.++ c d)) (str.len (str.++ c d e)))) (str.substr (str.++ c d e) 0 (- (str.len (str.++ c d e)) (str.len (str.++ c d))))))
@@ -1465,4 +1552,216 @@ mod tests {
             }
         }
     }
+
+    #[test]
+    fn string_decompose() {
+        test_cases! {
+            definitions = "
+                (declare-fun a () String)
+                (declare-fun b () String)
+                (declare-fun c () String)
+                (declare-fun d () String)
+            ",
+            "Simple working examples" {
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (false))"#: true,
+                r#"(assume h1 (>= (str.len (str.++ "d" "c")) 1))
+                   (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1))
+                   (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1)))
+                   (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_1) 1))) :rule string_decompose :premises (h1) :args (false))"#: true,
+                r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0))
+                   (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0))
+                   (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0)))
+                   (step t1 (cl (and (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2)) (= (str.len w_1) 0))) :rule string_decompose :premises (h1) :args (false))"#: true,
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= (str.++ "a" "b") (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: true,
+
+            }
+            "Reverse argument set to true" {
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: true,
+                r#"(assume h1 (>= (str.len (str.++ "d" "c")) 1))
+                   (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1))
+                   (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1)))
+                   (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_2) 1))) :rule string_decompose :premises (h1) :args (true))"#: true,
+            }
+            "Invalid argument type" {
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (1))"#: false,
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (1.5))"#: false,
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args ((- 1)))"#: false,
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args ("teste"))"#: false,
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (d))"#: false,
+            }
+            "Premise term \"t\" is not the same in the conclusion" {
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= "ba" (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: false,
+                r#"(assume h1 (>= (str.len "ba") 2))
+                   (define-fun w_1 () String (str.substr "ba" 0 2))
+                   (define-fun w_2 () String (str.substr "ba" 2 (- (str.len "ba") 2)))
+                   (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: false,
+                r#"(assume h1 (>= (str.len (str.++ "a" (str.++ b "c"))) 2))
+                   (define-fun w_1 () String (str.substr (str.++ "a" (str.++ b "c")) 0 2))
+                   (define-fun w_2 () String (str.substr (str.++ "a" (str.++ b "c")) 2 (- (str.len (str.++ "a" (str.++ b "c"))) 2)))
+                   (step t1 (cl (and (= (str.++ a (str.++ b "c")) (str.++ w_1 w_2)) (= (str.len w_2) 2))) :rule string_decompose :premises (h1) :args (true))"#: false,
+            }
+            "Switched skolems in the conclusion" {
+                r#"(assume h1 (>= (str.len (str.++ "d" "c")) 1))
+                   (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1))
+                   (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1)))
+                   (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_2 w_1)) (= (str.len w_1) 1))) :rule string_decompose :premises (h1) :args (false))"#: false,
+            }
+            "" {}
+            "Premise is not of the form (>= (str.len t) n)" {
+                r#"(assume h1 (< (str.len (str.++ "d" "c")) 1))
+                   (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1))
+                   (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1)))
+                   (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_2) 1))) :rule string_decompose :premises (h1) :args (true))"#: false,
+                r#"(assume h1 (>= (str.to_code (str.++ "d" "c")) 1))
+                   (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1))
+                   (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1)))
+                   (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_2) 1))) :rule string_decompose :premises (h1) :args (true))"#: false,
+            }
+            "Conclusion term is not of the form (and (= t x) (= (str.len y) 0))" {
+                r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0))
+                   (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0))
+                   (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0)))
+                   (step t1 (cl (or (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2)) (= (str.len w_1) 0))) :rule string_decompose :premises (h1) :args (false))"#: false,
+                r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0))
+                   (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0))
+                   (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0)))
+                   (step t1 (cl (and (not (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2))) (= (str.len w_1) 0))) :rule string_decompose :premises (h1) :args (false))"#: false,
+                r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0))
+                   (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0))
+                   (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0)))
+                   (step t1 (cl (and (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2)) (not (= (str.len w_1) 0)))) :rule string_decompose :premises (h1) :args (false))"#: false,
+                r#"(assume h1 (>= (str.len (str.++ a (str.++ "b" c))) 0))
+                   (define-fun w_1 () String (str.substr (str.++ a (str.++ "b" c)) 0 0))
+                   (define-fun w_2 () String (str.substr (str.++ a (str.++ "b" c)) 0 (- (str.len (str.++ a (str.++ "b" c))) 0)))
+                   (step t1 (cl (and (= (str.++ a (str.++ "b" c)) (str.++ w_1 w_2)) (= (str.to_code w_1) 0))) :rule string_decompose :premises (h1) :args (false))"#: false,
+            }
+            "Inverted argument value" {
+                r#"(assume h1 (>= (str.len "ab") 2))
+                   (define-fun w_1 () String (str.substr "ab" 0 2))
+                   (define-fun w_2 () String (str.substr "ab" 2 (- (str.len "ab") 2)))
+                   (step t1 (cl (and (= "ab" (str.++ w_1 w_2)) (= (str.len w_1) 2))) :rule string_decompose :premises (h1) :args (true))"#: false,
+                r#"(assume h1 (>= (str.len (str.++ "d" "c")) 1))
+                   (define-fun w_1 () String (str.substr (str.++ "d" "c") 0 1))
+                   (define-fun w_2 () String (str.substr (str.++ "d" "c") 1 (- (str.len (str.++ "d" "c")) 1)))
+                   (step t1 (cl (and (= (str.++ "d" "c") (str.++ w_1 w_2)) (= (str.len w_2) 1))) :rule string_decompose :premises (h1) :args (false))"#: false,
+            }
+        }
+    }
+
+    #[test]
+    fn string_length_pos() {
+        test_cases! {
+            definitions = "
+                (declare-fun a () String)
+                (declare-fun b () String)
+                (declare-fun c () String)
+                (declare-fun d () String)
+            ",
+            "Simple working examples" {
+                r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: true,
+                r#"(step t1 (cl (or (and (= (str.len (str.++ "a" (str.++ b "c"))) 0) (= (str.++ "a" (str.++ b "c")) "")) (> (str.len (str.++ "a" (str.++ b "c"))) 0))) :rule string_length_pos :args ((str.++ "a" (str.++ b "c"))))"#: true,
+                r#"(step t1 (cl (or (and (= (str.len a) 0) (= a "")) (> (str.len a) 0))) :rule string_length_pos :args (a))"#: true,
+                r#"(step t1 (cl (or (and (= (str.len (str.++ a "b")) 0) (= (str.++ a "b") "")) (> (str.len (str.++ a "b")) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: true,
+                r#"(step t1 (cl (or (and (= (str.len (str.++ "a" "b")) 0) (= (str.++ "a" "b") "")) (> (str.len (str.++ "a" "b")) 0))) :rule string_length_pos :args ("ab"))"#: true,
+            }
+            "Argument term \"t\" and the conclusion term \"t\" is not the same" {
+                r#"(step t1 (cl (or (and (= (str.len (str.++ a "b")) 0) (= (str.++ a "b") "")) (> (str.len (str.++ a "b")) 0))) :rule string_length_pos :args ((str.++ "a" b)))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len (str.++ "a" b)) 0) (= (str.++ "a" b) "")) (> (str.len (str.++ "a" b)) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len (str.++ "b" a)) 0) (= (str.++ a "b") "")) (> (str.len (str.++ a "b")) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len (str.++ a "b")) 0) (= a "")) (> (str.len (str.++ a "b")) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len (str.++ a "b")) 0) (= (str.++ a "b") "")) (> (str.len (str.++ b d)) 0))) :rule string_length_pos :args ((str.++ a "b")))"#: false,
+            }
+            "Conclusion is not of the form (or (and (= (str.len t) 0) (= t \"\")) (> (str.len t) 0))" {
+                r#"(step t1 (cl (and (and (= (str.len "ab") 0) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false,
+                r#"(step t1 (cl (or (or (= (str.len "ab") 0) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false,
+                r#"(step t1 (cl (or (and (not (= (str.len "ab") 0)) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false,
+                r#"(step t1 (cl (or (and (= (str.to_code "ab") 0) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len "ab") 1) (= "ab" "")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len "ab") 0) (not (= "ab" ""))) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "a")) (> (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "")) (< (str.len "ab") 0))) :rule string_length_pos :args ("ab"))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "")) (> (str.to_code "ab") 0))) :rule string_length_pos :args ("ab"))"#: false,
+                r#"(step t1 (cl (or (and (= (str.len "ab") 0) (= "ab" "")) (> (str.len "ab") 1))) :rule string_length_pos :args ("ab"))"#: false,
+            }
+        }
+    }
+
+    #[test]
+    fn string_length_non_empty() {
+        test_cases! {
+            definitions = "
+                (declare-fun a () String)
+                (declare-fun b () String)
+                (declare-fun c () String)
+                (declare-fun d () String)
+            ",
+            "Simple working examples" {
+                r#"(assume h1 (not (= "ab" "")))
+                   (step t1 (cl (not (= (str.len "ab") 0))) :rule string_length_non_empty :premises (h1))"#: true,
+                r#"(assume h1 (not (= (str.++ "a" (str.++ "b" "c")) "")))
+                   (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: true,
+                r#"(assume h1 (not (= d "")))
+                   (step t1 (cl (not (= (str.len d) 0))) :rule string_length_non_empty :premises (h1))"#: true,
+                r#"(assume h1 (not (= (str.++ b c) "")))
+                   (step t1 (cl (not (= (str.len (str.++ b c)) 0))) :rule string_length_non_empty :premises (h1))"#: true,
+                r#"(assume h1 (not (= (str.++ "b" "c") "")))
+                   (step t1 (cl (not (= (str.len "bc") 0))) :rule string_length_non_empty :premises (h1))"#: true,
+            }
+            "Premise term is not an inequality of the form (not (= t \"\"))" {
+                r#"(assume h1 (= (str.++ "a" (str.++ "b" "c")) ""))
+                   (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: false,
+                r#"(assume h1 (not (= (str.++ "a" (str.++ "b" "c")) "ab")))
+                   (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: false,
+                r#"(assume h1 (not (= (str.++ "a" (str.++ "b" "c")) a)))
+                   (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: false,
+                r#"(assume h1 (not (= (str.++ "a" (str.++ "b" "c")) (str.++ a b))))
+                   (step t1 (cl (not (= (str.len (str.++ "a" (str.++ "b" "c"))) 0))) :rule string_length_non_empty :premises (h1))"#: false,
+            }
+            "Shared term \"t\" between the premise and the conclusion is not the same" {
+                r#"(assume h1 (not (= (str.++ b c) "")))
+                   (step t1 (cl (not (= (str.len (str.++ c b)) 0))) :rule string_length_non_empty :premises (h1))"#: false,
+                r#"(assume h1 (not (= (str.++ b c) "")))
+                   (step t1 (cl (not (= (str.len (str.++ "b" "c")) 0))) :rule string_length_non_empty :premises (h1))"#: false,
+                r#"(assume h1 (not (= (str.++ "b" c) "")))
+                   (step t1 (cl (not (= (str.len (str.++ b c)) 0))) :rule string_length_non_empty :premises (h1))"#: false,
+            }
+            "Conclusion term is not an inequality of the form (not (= (str.len t) 0))" {
+                r#"(assume h1 (not (= "ab" "")))
+                   (step t1 (cl (= (str.len "ab") 0)) :rule string_length_non_empty :premises (h1))"#: false,
+                r#"(assume h1 (not (= "ab" "")))
+                   (step t1 (cl (not (= (str.to_code "ab") 0))) :rule string_length_non_empty :premises (h1))"#: false,
+                r#"(assume h1 (not (= "ab" "")))
+                   (step t1 (cl (not (> (str.len "ab") 0))) :rule string_length_non_empty :premises (h1))"#: false,
+                r#"(assume h1 (not (= "ab" "")))
+                   (step t1 (cl (not (= (str.len "ab") 1))) :rule string_length_non_empty :premises (h1))"#: false,
+            }
+        }
+    }
 }