Check sat assuming about dolmen HOT 2 CLOSED

The error is expected: as one can see in the smtlib spec (page 46), the syntax for check-sat-assuming is:

<prop_literal> ::= <symbol> | ( not <symbol> )
<command> =
  ...
  | ( check-sat-assuming ( <prop_literal>∗ ) )

Basically, check-sat-assuming does not take an arbitrary boolean term as payload, instead, it takes a list of propositional atoms. So when you open a parenthesis for the first (and only in this case) element of that list, the syntax states that it should be to write the negation of a boolean symbol, as stated by the hint.

from dolmen.

My bad, I relied on examples from the web that actually used check-sat-assuming with terms instead of symbols

from dolmen.