diff options
Diffstat (limited to 'test/regress/regress1/sygus/interpol_cosa_1.smt2')
| -rw-r--r-- | test/regress/regress1/sygus/interpol_cosa_1.smt2 | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/regress1/sygus/interpol_cosa_1.smt2 new file mode 100644 index 000000000..583f94ed4 --- /dev/null +++ b/test/regress/regress1/sygus/interpol_cosa_1.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --produce-interpols=conjecture --sygus-active-gen=enum --check-interpols +; SCRUBBER: grep -v -E '(\(define-fun)' +; EXIT: 0 +(set-logic ALL) +(set-option :produce-interpols conjecture) +(set-option :sygus-active-gen enum) +(declare-fun cfg@1 () (_ BitVec 1)) +(declare-fun witness_0@1 () Bool) +(declare-fun op@1 () (_ BitVec 4)) +(declare-fun counter@1 () (_ BitVec 16)) +(declare-fun input14@1 () (_ BitVec 1)) +(declare-fun clk@1 () (_ BitVec 1)) +(declare-fun a@1 () (_ BitVec 16)) +(declare-fun b@1 () (_ BitVec 16)) +(reset-assertions) +(declare-fun cfg@0 () (_ BitVec 1)) +(declare-fun witness_0@0 () Bool) +(declare-fun counter@0 () (_ BitVec 16)) +(declare-fun op@0 () (_ BitVec 4)) +(declare-fun input14@0 () (_ BitVec 1)) +(declare-fun b@0 () (_ BitVec 16)) +(declare-fun a@0 () (_ BitVec 16)) +(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) +(assert (and (or (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) witness_0@0) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) +(declare-fun cfg@2 () (_ BitVec 1)) +(declare-fun counter@2 () (_ BitVec 16)) +(declare-fun op@2 () (_ BitVec 4)) +(declare-fun witness_0@2 () Bool) +(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1))))) +(get-interpol I (not (and (and true (and (and (and (and true (= witness_0@2 (not (= (bvand (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@1 (_ bv0 4))) (bvadd a@1 b@1) (bvsub a@1 b@1)) (bvadd a@1 b@1)) input14@1))) (_ bv1 1))))) (= op@2 (ite (= cfg@1 (_ bv1 1)) (_ bv0 4) op@1))) (= counter@2 (bvadd counter@1 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@2 (_ bv0 1)))) (not witness_0@2)))) |