projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f10f495) | patch
Fix finiteness check for bounded fmf (#3589)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 4 Jan 2020 19:24:14 +0000 (13:24 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Sat, 4 Jan 2020 19:24:14 +0000 (11:24 -0800)
commite3e6f0dc62f0bb9d3fb8d752c5eb4600872fd806
treee61459b53e8bb8f8dd29c89655eb03f66e9dcfa4tree
parentf10f495cbb3784cfed51779836f49f7a06b4f289commit | diff
Fix finiteness check for bounded fmf (#3589)

Recently, finite model finding via uninterpreted sorts was decoupled from finite bound inference techniques (the BoundedIntegers module in theory/quantifiers/fmf/). This module assumed that finite model finding was enabled in one place. This fixes the issue by adding an additional check. This fixes a model unsoundness issue where bounds on an uninterpreted sort were not being enforced.

This fixes #3587.
src/theory/quantifiers/fmf/bounded_integers.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/fmf/issue3587.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/issue3537.smt2 diff | blob | history