Remove option to ignore negative memberships (#6665)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 2 Jun 2021 19:41:14 +0000 (12:41 -0700)
committerGitHub <noreply@github.com>
Wed, 2 Jun 2021 19:41:14 +0000 (19:41 +0000)
commit9258aa062ebefb8af7727567470f9a387181d466
tree7536a3775b50dd78f978e5a0d982f64182273651
parent85a300898d7815973c064fe2c7b5b33473a71a5c
Remove option to ignore negative memberships (#6665)

Fixes #6661. The option `--strings-inm` could be used to ignore negative
membership constraints. However, this option made the string solver
model-unsound or produced incorrect models if the user provided a
benchmark that actually contained negative membership constraints. The
solver did not check for negative membership constraints and did not
warn the user about them. Because the option is not really being used,
this commit removes it.
src/options/strings_options.toml
src/theory/strings/regexp_solver.cpp
test/regress/regress1/strings/regexp002.smt2