blob: fbd200f66bd536877cb1e301bfc30696ed455756 (
plain)
1
2
3
4
5
6
7
8
9
|
; COMMAND-LINE: --decision=justification
; EXPECT: sat
(set-logic AUFLRA)
(declare-fun _substvar_323_ () Bool)
(declare-sort S0 0)
(declare-const arr-8825057447867329665_7821057345541224443-0 (Array Bool S0))
(declare-const arr--3985848114402943554_-2673408464765268945-0 (Array Real (Array Bool S0)))
(assert (not (= (select arr--3985848114402943554_-2673408464765268945-0 0.0) (store (store arr-8825057447867329665_7821057345541224443-0 _substvar_323_ (select arr-8825057447867329665_7821057345541224443-0 true)) false (select arr-8825057447867329665_7821057345541224443-0 false)) arr-8825057447867329665_7821057345541224443-0 arr-8825057447867329665_7821057345541224443-0)))
(check-sat)
|
