projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 12ff841) | patch
Fix sort inference for equality over finite types (#8897)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 22 Jun 2022 18:16:00 +0000 (13:16 -0500)
committerGitHub <noreply@github.com>
Wed, 22 Jun 2022 18:16:00 +0000 (13:16 -0500)
commitebc7d0ffafe9736ecab5649d2a3957e55e06c515
treeebe7ee3e969f8222c20841c0f9160f07a44a8d10tree
parent12ff8418d65db0ddbf53035100652d9f645d71fccommit | diff
Fix sort inference for equality over finite types (#8897)

Sort inference for equality was not considering equality over some finite types, leading to potential solution soundness.

Fixes #8883.
src/theory/sort_inference.cpp diff | blob | history
src/theory/sort_inference.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2 [new file with mode: 0644] blob