Check sat assuming

[Stevendeo]

The following example fails :

(set-logic ALL)

(declare-const x Int)
(assert (= x 4))

(check-sat-assuming ((= x 3)))

with the error message:

File "test.smt2", line 6, character 22-23:
6 | (check-sat-assuming ((= x 3)))
                          ^
Error expected the 'not' symbol at that point.
      Hint: check-sat-assuming only accepts a list of terms of the form 'p'
            or '(not p)', where p is a boolean literal.

[Gbury]

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.

[Stevendeo]

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