diff options
Diffstat (limited to 'test/regress/regress1/sygus/issue3649.sy')
-rw-r--r-- | test/regress/regress1/sygus/issue3649.sy | 24 |
1 files changed, 24 insertions, 0 deletions
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) |