check for null assumption in query and replace with false (#2858)
authormakaimann <makaim@stanford.edu>
Thu, 14 Mar 2019 07:08:15 +0000 (00:08 -0700)
committerAndres Noetzli <andres.noetzli@gmail.com>
Thu, 14 Mar 2019 07:08:15 +0000 (07:08 +0000)
commit1744dc5f3140f9dc2aeb71f99c530feb83264a04
treef1a651a00059640e03e80ad620afb7bc8b0bc4b6
parentb574ccf82270f8887d2d697c537c591ff4ab68a2
check for null assumption in query and replace with false (#2858)

The default assumption argument in query was a null `Expr`, but the implementation asserted that the assumption is not null:

declaration: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.h#L593
implementation: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3548

The change is to simply check if the assumption is null and replaces it with the `false` expression if it is.

It should be `false` not `true` because it is negated in checkSatisfiability (when it's a query) as seen here: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3607

Note: I couldn't find a clean way to make `false` the default argument of assumption, because the expression manager is non-static.
src/smt/smt_engine.cpp