mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
add regression test
This commit is contained in:
parent
c9127c6cd7
commit
f024fe821e
1 changed files with 10 additions and 0 deletions
10
tests/sat/reg_2022-09-10.smt2
Normal file
10
tests/sat/reg_2022-09-10.smt2
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
|
||||
; 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)
|
||||
Loading…
Add table
Reference in a new issue