From f38cd31ddfd3d5caa2ffe3a0ffafbb2b0394391b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 12 Feb 2020 16:24:13 -0600 Subject: Ensure ext rewrites for associative ops dont throw assertions for kind arities (#3681) --- test/regress/regress1/sygus/issue3649.sy | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test/regress/regress1/sygus/issue3649.sy (limited to 'test/regress/regress1/sygus/issue3649.sy') diff --git a/test/regress/regress1/sygus/issue3649.sy b/test/regress/regress1/sygus/issue3649.sy new file mode 100644 index 000000000..12949c55a --- /dev/null +++ b/test/regress/regress1/sygus/issue3649.sy @@ -0,0 +1,24 @@ +; EXPECT: unknown +; COMMAND-LINE: --sygus-out=status +(set-logic ALL) +(synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool) + +(define-fun init-fn ((i Int) (x (Array Int Int)) (c Int)) Bool + (and (= i 0) + (= (select x 10) c))) + +(define-fun post-fn ((i Int) (x (Array Int Int))(c Int)) Bool + (exists ((index Int)) (and (= (select x index) c) + (forall ((index2 Int)) (=> (< index2 index) (not (= (select x index) c)))) + ))) + +(declare-var x (Array Int Int)) +(declare-var x! (Array Int Int)) +(declare-var i Int) +(declare-var i! Int) +(declare-var c Int) + + +(constraint (=> (init-fn i x c) (inv-fn i x c))) +(constraint (=> (inv-fn i x c) (post-fn i x c))) +(check-synth) -- cgit v1.2.3