test/regress/regress0/proof_no_support.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

;COMMAND-LINE: --check-proofs
;EXIT: 1
;EXPECT: (error "Error in option parsing: Proofs are only supported for sub-logics of QF_AUFBVLIA.")
(set-logic ALL)

(declare-const a Int)

(assert (and 
          (=
            a
            (* a a)
          )
          (not (= a 0))
          (not (= a 1))
        )
)

(check-sat)