Require that FMF model basis terms are variables (#3031)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 1 Jun 2019 07:39:16 +0000 (09:39 +0200)
committerAndres Noetzli <andres.noetzli@gmail.com>
Sat, 1 Jun 2019 07:39:16 +0000 (00:39 -0700)
commit9b6985b4427aff888f07ecc84079452c11113cb6
treee693faec20af263356c78ee7daa7bb5340b307f7
parent9d93595783e350969ad428ab277614a3250e59a0
 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.
src/theory/quantifiers/first_order_model.cpp
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h