projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 75d15b2) | patch
a formula should be an instance of itself (#1668)
authoryoni206 <yoni206@users.noreply.github.com>
Mon, 2 Apr 2018 21:15:02 +0000 (14:15 -0700)
committerGitHub <noreply@github.com>
Mon, 2 Apr 2018 21:15:02 +0000 (14:15 -0700)
commit065adbb66136022236efb73af740ff6b2c0f178a
tree1abcf462bb6fd175d7a5542bcbd9a1a555333543tree
parent75d15b2cd923f92fd26020e0c8d1786b4396d608commit | diff
a formula should be an instance of itself (#1668)

Proof checking failed when applying the instantiation rule so that the original formula and the instantiated formula are the same. Fixed using the new "ifequal" construct in lfsc.
proofs/signatures/th_quant.plf diff | blob | history