diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-06-01 09:39:16 +0200 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-01 00:39:16 -0700 |
| commit | 9b6985b4427aff888f07ecc84079452c11113cb6 (patch) | |
| tree | e693faec20af263356c78ee7daa7bb5340b307f7 /src/smt_util | |
| parent | 9d93595783e350969ad428ab277614a3250e59a0 (diff) | |
Require that FMF model basis terms are variables (#3031)
The commit fixes an issue where FMF could theoretically chose interpreted function applications as "model basis terms". This triggered an incorrect model (caught by an AlwaysAssert) when the interpreted function later did not appear in a model and was chosen by FMF to be equal to a wrong value.
Diffstat (limited to 'src/smt_util')
0 files changed, 0 insertions, 0 deletions