diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-19 19:28:08 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-19 19:28:08 -0600 |
| commit | c8e8acd26b4bd5c47110b9448a74a45913b5518f (patch) | |
| tree | 91a27c3e9269e2ff4f852fb7b4d7475e00826ef0 /.github | |
| parent | 3c754308f66d92cd4b03d5f159464585c315b528 (diff) | |
Use arbitrary ground term assignment for sorts where isInterpretedFinite is true (#5790)
This makes a small change to our model construction to assign arbitrary values to eqc for types that are "interpreted finite", that is, have finite cardinality under the assumption that uninterpreted sorts are finite/infinite (when finite model finding is on/off). Uninterpreted sorts themselves always use the type enumerator to assign distinct values.
This fixes #5738.
This change is necessary since there was previously a mismatch between types where isFinite != isInterpretedFinite, in particular a datatype with a single constructor with a unintepreted type field as in that issue.
Diffstat (limited to '.github')
0 files changed, 0 insertions, 0 deletions