projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: aba70eb) | patch
Fix spurious assertion failure (#8404)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 26 Mar 2022 03:46:31 +0000 (22:46 -0500)
committerGitHub <noreply@github.com>
Sat, 26 Mar 2022 03:46:31 +0000 (03:46 +0000)
commitd49f537e5bc394d9b6e6728c1875062aa2b1e39c
tree35932be8143f8ff178ba195ce663e5312148124ctree
parentaba70eb79f255582aa5c254518b3731f284ad0c4commit | diff
Fix spurious assertion failure (#8404)

This was wrong when doing sequences of reals and a seq.nth merges with a seq.len.

Fixes cvc5/cvc5-projects#502.
src/theory/strings/eager_solver.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress1/strings/proj-issue502-merge-type.smt2 [new file with mode: 0644] blob