(z3str3) Assertion Violation in theory_str_mc.cpp with replacing empty Strings

Z3Prover / z3

The Z3 Theorem Prover

Other

10.42k stars 1.47k forks source link

(z3str3) Assertion Violation in theory_str_mc.cpp with replacing empty Strings #4486

Closed dylanjwolff closed 4 years ago

dylanjwolff commented 4 years ago

Hi, I found the following formula throws an assertion violation with the z3str3 solver on the release and debug builds:

bug.smt2.gz

%  z3 smt.string_solver=z3str3 bug.smt2 
ASSERTION VIOLATION
File: ../src/smt/theory_str_mc.cpp
Line: 728
Failed to verify: pos_exists

% cat bug.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () Int)
(assert (= (str.replace "" (str.at "" c) "") (str.replace a b "")))
(check-sat)

Verified on master, commit: c967b4a OS: Ubuntu 18.04

mtrberzi commented 4 years ago

Seems like the problem might be with str.at, but I can resolve this for you.

mtrberzi commented 4 years ago

Opened #4490.