'div' not declared and re.loop isn't working. probably because regex isn't in CVC4 :(

cvc4_string_errors_02.smt2

(set-logic QF_S)
(declare-const str_a String)
(declare-const str_b String)
(declare-const str_c String)
(assert (= 
    (str.len str_c) 
    0))
(assert (= 
    (str.len str_c) 
    2))
(assert (<= (* 47 (div (str.indexof str_b "GM" 0) 337824)) 566))
(assert (str.in.re str_c 
    (re.union ((_ re.loop 0 2) (str.to.re "bVGMs")) ((_ re.loop 2 3) (re.union (re.range "a" "d") (str.to.re "NNs"))))))
(assert (or 
    (str.contains "" "bV") 
    (>= (+ (str.indexof str_a str_b 4) 505) (- 220320))))
(assert (not (str.in.re (str.++ 
        "GM" 
        "") 
      (re.union ((_ re.loop 0 2) (str.to.re "bVGMs")) ((_ re.loop 2 3) (re.union (re.range "a" "d") (str.to.re "NNs")))))))
(assert (< (str.len (str.replace (str.++ 
          "GM" 
          str_c) 
        str_a 
        (str.replace str_a 
          "" 
          str_b))) (str.len (str.++ 
        str_b 
        str_a))))
(check-sat)


ERRORS:

(error "Parse Error: <shell>:1.21: Symbol 'div' not declared as a variable")

(error "Parse Error: <shell>:2.25: Unknown indexed function `re.loop'

      (re.union ((_ re.loop 0 2) (str.to.re "bVGMs")) ((_ re.loop 2 3) (...
                    ^
")

(error "Parse Error: <shell>:4.27: Unknown indexed function `re.loop'

        (re.union ((_ re.loop 0 2) (str.to.re "bVGMs")) ((_ re.loop 2 3)...
                      ^
")