test/regress/regress3/unbdd_inv_gen_ex7.sy

   1 ; EXPECT: unsat
   2 ; COMMAND-LINE: --lang=sygus2 --sygus-out=status
   3 (set-logic LIA)
   4 (synth-fun inv ((i Int) (y Int) (l Int)) Bool
   5     ((Start Bool) (AtomicFormula Bool) (Sum Int) (Term Int) (Sign Int) (Var Int) (Const Int))
   6     (
   7         (Start Bool ((and AtomicFormula AtomicFormula)
   8                      (or AtomicFormula AtomicFormula)))
   9         (AtomicFormula Bool ((<= Sum Const) (= Sum Const)))
  10         (Sum Int ((+ Term Term)))
  11         (Term Int ((* Sign Var)))
  12         (Sign Int (0 1 (- 1)))
  13         (Var Int (i y l))
  14         (Const Int ((+ Const Const) (- Const Const) 0 1))
  15     )
  16 )
  17
  18 (define-fun implies ((b1 Bool) (b2 Bool)) Bool (or (not b1) b2))
  19 (define-fun and3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (and (and b1 b2) b3))
  20 (define-fun and4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (and (and3 b1 b2 b3) b4))
  21 (define-fun and5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (and (and4 b1 b2 b3 b4) b5))
  22 (define-fun and6 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool) (b6 Bool)) Bool (and (and5 b1 b2 b3 b4 b5) b6))
  23 (define-fun or3 ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (or (or b1 b2) b3))
  24 (define-fun or4 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool)) Bool (or (or3 b1 b2 b3) b4))
  25 (define-fun or5 ((b1 Bool) (b2 Bool) (b3 Bool) (b4 Bool) (b5 Bool)) Bool (or (or4 b1 b2 b3 b4) b5))
  26
  27 (declare-var i Int)
  28 (declare-var x Int)
  29 (declare-var y Int)
  30 (declare-var l Int)
  31 (declare-var i1 Int)
  32 (declare-var x1 Int)
  33 (declare-var y1 Int)
  34 (declare-var l1 Int)
  35
  36 (constraint (implies (or3 (< x 0) (< y 0) (> y x)) true))
  37 (constraint (implies (and3 (not (or3 (< x 0) (< y 0) (> y x))) (= l x) (= i 0)) (inv i y l)))
  38 (constraint (implies (and4 (inv i y l) (< i y) (not (or (< i 0) (>= i l))) (= i1 (+ i 1))) (inv i1 y l)))
  39 (constraint (implies (and3 (inv i y l) (< i y) (or (< i 0) (>= i l))) false))
  40
  41 (check-synth)