projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 45a5d52) | patch
Fix fmf-fun for non-equality function definitions (#2134)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 4 Jul 2018 05:21:01 +0000 (00:21 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 4 Jul 2018 05:21:01 +0000 (22:21 -0700)
commitfad7a9aafa35210bb8b685261ec1caae2c7e0624
tree71e410d4778ac9fe463a2dad3dcb2b267a0a6797tree
parent45a5d525d26dba9ed3f12d888c8b9fb844c8a8eccommit | diff
Fix fmf-fun for non-equality function definitions (#2134)

Fixes #2133. In that issue, a quantifiers rewrite triggered a model-unsoundness in fmf-fun. The rewrite made a function definition have an ITE at top-level instead of equality. The corrected code was model-unsound, since it assumed that quantified formulas that are not EQUAL can be ignored.
src/theory/quantifiers/fun_def_process.cpp diff | blob | history