Closed zhendongsu closed 1 year ago
OS: Ubuntu 18.04 Commit: https://github.com/cvc5/cvc5/commit/cc8071138e5b9647483400af303eab9497c9913e
[539] % cvc5 -i -q --check-models small.smt2 sat Fatal failure within void cvc5::internal::smt::CheckModels::checkModel(cvc5::internal::theory::TheoryModel*, const cvc5::context::CDList<cvc5::internal::NodeTemplate<true> >&, bool) at /local/suz-local/software/CVC4/src/smt/check_models.cpp:134 Internal error detected SolverEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL: assertion: (let ((_let_1 (d T))) (= (n v t) (ite ((_ is T) (n 0 T)) T (RB (RB o (BT _let_1) (RBT _let_1) (r _let_1)))))) simplifies to: false expected `true'. Run with `--check-models -v' for additional diagnostics. Aborted [540] % cat small.smt2 (declare-datatypes ((C 0)) (((C) (o)))) (declare-datatypes ((R 0) (RB 0)) (((T) (RB (d RB))) ((RB (B C) (BT R) (RBT Int) (r R))))) (declare-datatypes ((B 0)) (((B (B Bool))))) (declare-fun v () Int) (declare-fun t () R) (declare-fun n (Int R) R) (declare-fun N (R) B) (assert (and (not ((_ is T) (n v t))) (not (B (N (BT (d (n v t)))))))) (check-sat) (assert (= (n v t) (ite ((_ is T) (n 0 T)) T (RB (RB o (BT (d T)) (RBT (d T)) (r (d T))))))) (check-sat)
It appears that the model is correct, but our model evaluation may be incorrect, likely due to incorrectly applied selectors.
OS: Ubuntu 18.04 Commit: https://github.com/cvc5/cvc5/commit/cc8071138e5b9647483400af303eab9497c9913e