Jongwook_Kim
Jongwook_Kim
I try to resolve with your solution. Thank you for answer!
Thanks for taking the time.
another is z3str3 with str.replace, str.substr. ``` $ z3 smt.string_solver=z3str3 small.smt2 unsat $ z3 small.smt2 sat $ cat small.smt2 (set-logic QF_SLIA) (declare-fun v () String) (declare-fun g () Int) (assert...
Even if formula is satisfiable, z3str3 always returns ``unsat`` when variable or function is parameter of ``re.range``. ``` $ z3 smt.string_solver=z3str3 small.smt2 unsat $ z3 small.smt2 sat $ cat small.smt2...