mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-05 19:00:33 -05:00
10 lines
238 B
Text
10 lines
238 B
Text
|
|
; falsly declared unsat. minimized
|
|
; from tests/sat/QF_UF_schedule_world.2.prop1_ab_cti_max.smt2 using ddSMT .
|
|
(declare-fun p () Bool)
|
|
(declare-fun y () Bool)
|
|
(assert (= false (not p)))
|
|
(assert p)
|
|
(assert (= y p))
|
|
(assert y)
|
|
(check-sat)
|