blob: 5a01e44f8f704ed973cb52e20396e64759b8576a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
; COMMAND-LINE: --incremental
(set-logic UF)
(set-option :produce-unsat-assumptions true)
(declare-fun _substvar_4_ () Bool)
(check-sat-assuming (_substvar_4_ (= _substvar_4_ _substvar_4_)))
; EXPECT: sat
(check-sat-assuming (_substvar_4_ false))
; EXPECT: unsat
(get-unsat-assumptions)
; EXPECT: [false]
(check-sat-assuming ((= _substvar_4_ _substvar_4_) (distinct _substvar_4_ _substvar_4_)))
; EXPECT: unsat
(get-unsat-assumptions)
; EXPECT: [(distinct _substvar_4_ _substvar_4_)]
|
