projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 217a258) | patch
Fix preregistration for floating point theory (#7558)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 3 Nov 2021 10:27:20 +0000 (05:27 -0500)
committerGitHub <noreply@github.com>
Wed, 3 Nov 2021 10:27:20 +0000 (10:27 +0000)
commit324434a74b35d0e58bdb551c9155e9fb32844d07
treeef0cc6130cf87c7cfa0f1461925dea6315f9a03ftree
parent217a258f4b52d8776c344f9c3d0d9e79aec060a5commit | diff
Fix preregistration for floating point theory (#7558)

Preregistering terms must always add them to the equality engine of TheoryFp, otherwise there may be preregistered terms that do not occur in the equality engine of TheoryFp, thus leading to crashes during theory combination.

Fixes cvc5/cvc5-projects#329.
src/theory/fp/theory_fp.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/fp/proj-issue329-prereg-context.smt2 [new file with mode: 0644] blob