diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2018-04-02 14:15:02 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-02 14:15:02 -0700 |
| commit | 065adbb66136022236efb73af740ff6b2c0f178a (patch) | |
| tree | 1abcf462bb6fd175d7a5542bcbd9a1a555333543 /src/theory/quantifiers/sygus/sygus_unif.h | |
| parent | 75d15b2cd923f92fd26020e0c8d1786b4396d608 (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.
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif.h')
0 files changed, 0 insertions, 0 deletions