test/regress/regress0/proof_no_support.smt2

   1 ;COMMAND-LINE: --check-proofs
   2 ;EXIT: 1
   3 ;EXPECT: (error "Error in option parsing: Proofs are only supported for sub-logics of QF_AUFBVLIA.")
   4 (set-logic ALL)
   5
   6 (declare-const a Int)
   7
   8 (assert (and
   9           (=
  10             a
  11             (* a a)
  12           )
  13           (not (= a 0))
  14           (not (= a 1))
  15         )
  16 )
  17
  18 (check-sat)
  19
  20
  21