projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 187bbe0) | patch
Fix refutational soundness bug in quantifier prenexing (#6448)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 27 Apr 2021 21:25:11 +0000 (16:25 -0500)
committerGitHub <noreply@github.com>
Tue, 27 Apr 2021 21:25:11 +0000 (21:25 +0000)
commitd524948b58c4c3f61c623649049f6209b7756ed6
treeed35c98dbcb5428b9e4ba6db18f891df985ab1a3tree
parent187bbe04f54798f84b404dc61d2a9d221130109dcommit | diff
Fix refutational soundness bug in quantifier prenexing (#6448)

This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas.

This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables.

This was reported by Geoff Sutcliffe via a TPTP run.
src/expr/bound_var_manager.cpp diff | blob | history
src/expr/bound_var_manager.h diff | blob | history
src/theory/quantifiers/quantifiers_macros.cpp diff | blob | history
src/theory/quantifiers/quantifiers_macros.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/macro-geo-small-3.smt2 [new file with mode: 0644] blob