diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-04 02:12:02 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-04 00:12:02 -0700 |
| commit | 472c5a592c78e4757b3201f9e20908a4c645921b (patch) | |
| tree | 43aa40d426af3d8b05fd358951601a1eecbf25ff /test/regress/regress1/sygus/bvudiv-by-2.sy | |
| parent | 167947ab81094de28251bb885c8cf84e7168c43b (diff) | |
Avoid duplicate lemmas in datatypes (#3310)
We previously were sending e.g. dt.size >= 0 lemmas when size terms are pre-registered, which can happen multiple times in a user context. This ensures we cache whether a lemma is sent in a user-context dependent way in the datatypes solver. This ensures we don't send the same lemma twice for dt.size >= 0 lemmas.
Diffstat (limited to 'test/regress/regress1/sygus/bvudiv-by-2.sy')
0 files changed, 0 insertions, 0 deletions