From 90cdbec9bdac0e00053f702868983c21572d6eb3 Mon Sep 17 00:00:00 2001 From: Alexander Nutz Date: Mon, 27 Mar 2017 16:02:02 +0200 Subject: [PATCH] adding a horn clause smt script that we cannot parse, see #18 --- .../horn/test-implicitInitialTransitions.smt2 | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 trunk/examples/smtlib/horn/test-implicitInitialTransitions.smt2 diff --git a/trunk/examples/smtlib/horn/test-implicitInitialTransitions.smt2 b/trunk/examples/smtlib/horn/test-implicitInitialTransitions.smt2 new file mode 100644 index 00000000000..b18dd4e8076 --- /dev/null +++ b/trunk/examples/smtlib/horn/test-implicitInitialTransitions.smt2 @@ -0,0 +1,19 @@ +; status: sat (checked by z3) +; written on 27.03.2017 +; currently, we say this set is sat without looking at any trace, because the "initial transitions" +; don't have the form of an implication withough uninterpreted predicates in the body. +(set-logic HORN) + +(declare-fun I_x (Int) Bool) +(declare-fun I_y (Int) Bool) +(declare-fun I_z (Int) Bool) + +(assert (I_x 0)) ; equivalent to "(=> (= x 0) (I_x x))", but not translated like that right now.. +(assert (I_y 0)) +(assert (forall ((x Int) (x1 Int)) (=> (and (I_x x) (= x1 (+ x 1))) (I_x x1)))) +(assert (forall ((y Int) (y1 Int)) (=> (and (I_y y) (= y1 (+ y 1))) (I_y y1)))) + +(assert (forall ((x Int) (y Int) (z Int)) (=> (and (I_x x) (I_y y) (= (+ x y) z)) (I_z z)))) +(assert (forall ((z Int)) (=> (and (I_z z) (< z 0)) false))) + +(check-sat)