Assertion violation at smtrat-modules/SATModule/mcsat/MCSATMixin.tpp:170

[rainoftime]

(set-logic QF_UF)
(declare-fun _substvar_18_ () Bool)
(declare-sort S2 0)
(declare-fun S2-1 () S2)
(declare-fun v32 () Bool)
(assert (or (= S2-1 S2-1) v32))
(assert (or v32 _substvar_18_))
(check-sat)

smtrat 0e70dd2

smtrat-shared: /home/smtrat/src/smtrat-modules/SATModule/mcsat/MCSATMixin.tpp:170: std::pair<boost::logic::tribool, boost::optional<boost::variant<carl::Formula<carl::MultivariatePolynomial<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > >, smtrat::mcsat::ClauseChain> > > smtrat::mcsat::MCSATMixin<Settings>::propagateBooleanDomain(Minisat::Lit) [with Settings = smtrat::mcsat::MCSATSettingsFMICPVSOC]: Assertion `vars.size() > 0' failed.

set(SMTRAT_Strategy "MCSATFMICPVSOC" CACHE STRING "Used strategy in the solver")

[nafur]

The MCSAT strategy does not support uninterpreted sorts at all.