add testcase with both cyclic and acyclic constraint

src/Language/Fixpoint/Horn/Transformations.hs

@@ -779,6 +779,8 @@ substPred su (Var k xs) = Var k $ upd <$> xs
 -- (and (forall ((x int) (x > 0)) (and (forall ((y int) (y > x + 100)) (forall ((v int) (v == x + y)) ((true)))) (forall ((y int) (y > x + 100)) (forall ((v int) (v == x + y)) (forall ((z int) (z == v)) (forall ((v int) (v == x + z)) ((v > 100)))))))))
 -- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test03.smt2"
 -- (and (and (forall ((x int) (x > 0)) (forall ((v int) (v == x)) (($k0 v)))) (forall ((y int) ($k0 y)) (forall ((v int) (v == y + 1)) (($k0 v)))) (forall ((z int) ($k0 z)) ((z > 0)))))
+-- >>> elim defConfig . fst <$> parseFromFile hornP "tests/horn/pos/test04.smt2"
+-- (and (forall ((x int) (x > 0)) (forall ((v int) (v == x)) (($k0 v)))) (forall ((y int) ($k0 y)) (forall ((yyy int) (true)) (forall ((vvv int) (vvv == yyy + 1)) (forall ((v int) (and (v == vvv) (y == yyy))) (($k0 v)))))) (forall ((z int) ($k0 z)) ((z > 0))))
 ------------------------------------------------------------------------------
 elim :: (F.PPrint a) => F.Config -> Query a -> Cstr a
 ------------------------------------------------------------------------------

tests/horn/pos/test04.smt2

@@ -0,0 +1,20 @@
+// TODO move to actual SMTLIB format 
+
+(var $k0 ((Int)))
+(var $k1 ((int) (int)))
+
+(qualif Foo ((v Int)) ((v > 0)))
+
+(constraint 
+  (and 
+    (forall ((yyy Int) (true))  
+       (forall ((vvv Int) (vvv = yyy + 1)) 
+          (($k1 vvv yyy))))
+    (forall ((x Int) (x > 0))
+      (forall ((v Int) (v = x)) 
+        (($k0 v))))
+    (forall ((y Int) ($k0 y))
+        (forall ((v Int) ($k1 v y)) 
+          (($k0 v))))
+    (forall ((z Int) ($k0 z))
+        ((z > 0)))))