Regression with existential quantifier elimination?

[wintered]

Commit: 6394bf6
OS: Ubuntu 18.04

$cvc5 -q --strings-exp f1.smt2
unknown
(not (and (forall ((BOUND_VARIABLE_2284 Int)) (not (>= (str.len 
(str.substr (str.replace_re "" (str.to_re v) v) BOUND_VARIABLE_2284 1)) 1))) (not u)))
$cvc4-1.8 -q --strings-exp f1.smt2
sat
true
$cat f1.smt2 
(declare-const u Bool)
(declare-fun v () String)
(assert   (exists ((x Int)) (or (not (>= 0 (str.len (str.substr 
          (str.replace_re "" (str.to_re v) v) x 1)))) u)))
(check-sat)
(simplify (exists ((x Int)) (or (not (>= 0 (str.len (str.substr 
          (str.replace_re "" (str.to_re v) v) x 1)))) u)))

cvc5 rewrites the existential quantifier to an universal quantifier while cvc4-1.8 simplifies the whole term to true.

[wintered]

cvc5 can decide the same formula if the existential quantification of x is implicit.

$cvc5 -q --strings-exp f2.smt2
sat
(or (>= (str.len (str.substr (str.replace_re "" (str.to_re v) v) x 1)) 1) u)
$cat f2.smt2                  
(declare-const u Bool)
(declare-fun v () String)
(declare-fun x () Int)
(assert   (or (not (>= 0 (str.len (str.substr 
          (str.replace_re "" (str.to_re v) v) x 1)))) u))
(check-sat)
(simplify (or (not (>= 0 (str.len (str.substr 
          (str.replace_re "" (str.to_re v) v) x 1)))) u))

[ajreynol]

We should consider applying some form of --pre-skolem-quant by default.