projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c501613) | patch
Fix injectivity inferences for seq.nth applied to strings (#8920)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 30 Jun 2022 09:39:42 +0000 (04:39 -0500)
committerGitHub <noreply@github.com>
Thu, 30 Jun 2022 09:39:42 +0000 (09:39 +0000)
commit0bf059f7969670d76f947086c3bc5e7688f2903e
tree7faa751d08602c65f43296cdfebbb30f49b17441tree
parentc501613c172412b579884b37ed3133a8bbb06f09commit | diff
Fix injectivity inferences for seq.nth applied to strings (#8920)

Fixes #8916.
src/theory/strings/base_solver.cpp diff | blob | history
src/theory/strings/base_solver.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress1/strings/issue8916-str-unit-pairs.smt2 [new file with mode: 0644] blob