projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b9308b9) | patch
[Strings] Avoid trivial explanation (#7982)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 25 Jan 2022 04:33:13 +0000 (20:33 -0800)
committerGitHub <noreply@github.com>
Tue, 25 Jan 2022 04:33:13 +0000 (04:33 +0000)
commit18c55e25574ef9dab5af7cdb86ad497d97b40911
tree03aea0976ab2d86f114ecf037711b90b3a3dffa1tree
parentb9308b9b9cf07b02318d772a508781971603be2ccommit | diff
[Strings] Avoid trivial explanation (#7982)

The `STRINGS_N_UNIFY` inference could produce trivial explanations. For
example, if both `x` and `y` were of kind `seq.unit`, then the
explanation was `(= 1 1)`. This lead to issues when checking proofs.
src/theory/strings/core_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress2/seq/err-model-soundness.smt2 [new file with mode: 0644] blob