mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

Add few more testcases

Browse source
This commit is contained in:
Huanyi Chen 2018-12-28 13:24:39 -05:00
parent 300e99b67a
commit 4b29b208ad
5 changed files with 433 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

17
examples/python/data/horn3.smt2 Normal file
View file

@ -0,0 +1,17 @@
(declare-rel Invariant (Bool))
(declare-rel Goal ())
(declare-var l0 Bool)
(declare-var l2 Bool)
(declare-var l4 Bool)
(declare-var l6 Bool)
(declare-var l8 Bool)
(declare-var l10 Bool)
(rule (=> (not (or l4)) (Invariant l4)))
(rule (=> (and (Invariant l4)
(= (and (not l4) (not l2)) l6)
(= (and l4 l2) l8)
(= (and (not l8) (not l6)) l10)
) (Invariant l10)))
(rule (=> (and (Invariant l4)
l4) Goal))
(query Goal)