Skip to content

Refutational soundness bug on string formula #5071

Closed
@wintered

Description

Commit: 11efe33

$z3release model_validate=true bug.smt2
unsat
$cvc4 -q bug.smt2                                 
sat
$cat bug.smt2 
(assert (= "bZAHP6GSLAbZAHP6GSLAbZAHP6GSLAbZAHP6GSLA" 
        (str.replace_all "bZAHP6GSLAbZAHP6GSLA" "bZAHP6GSLA" "bZAHP6GSLAbZAHP6GSLA"))) 
(check-sat)

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions