--check-models Fatal failure at CVC4/src/smt/smt_engine.cpp:4738

[muchang]

Hi,
For this formula,

(declare-fun a () Real)
(assert (= a (sin 1.0)))
(check-sat)

cvc4 --check-models throws out a fatal failure:

Fatal failure within void CVC4::SmtEngine::checkModel(bool) at CVC4/src/smt/smt_engine.cpp:4738
Internal error detectedSmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:
model value for a
             is (sin 1)
and that is not a constant (.isConst() == false).
Run with `--check-models -v' for additional diagnostics.
Aborted

with `--check-models -v' :

minisat: Incremental solving is forced on (to avoid variable elimination) unless using internal decision strategy.
============================[ Search Statistics ]==============================
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
===============================================================================
===============================================================================
SmtEngine::checkModel(): generating model
(model
Fatal failure within CVC4::Expr CVC4::SmtEngine::getValue(const CVC4::Expr&) const at CVC4/src/smt/smt_engine.cpp:4283
Check failure
 m->hasApproximations() || resultNode.getKind() == kind::LAMBDA || resultNode.isConst()
Aborted

OS: Ubuntu 18.04
Revision: 618282e

[ajreynol]

Due to transcendental functions not being considered approximations, thus our assertion is still too strong.