diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-23 15:53:48 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-23 15:53:48 -0600 |
commit | dd29958ff0c78c099f540f080e455d843caf1c6b (patch) | |
tree | 4f3d6edfdb60463eff7c22001220adddebd30b81 /test | |
parent | fd88b18c0db55eb63d0cd0454b19810a8abee789 (diff) |
Fix trivial solve method for single invocation (#3650)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/issue3654.sy | 24 |
2 files changed, 25 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 65d7f2b31..518e3a889 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1787,6 +1787,7 @@ set(regress_1_tests regress1/sygus/issue3580.sy regress1/sygus/issue3634.smt2 regress1/sygus/issue3635.smt2 + regress1/sygus/issue3654.sy regress1/sygus/large-const-simp.sy regress1/sygus/let-bug-simp.sy regress1/sygus/list-head-x.sy diff --git a/test/regress/regress1/sygus/issue3654.sy b/test/regress/regress1/sygus/issue3654.sy new file mode 100644 index 000000000..12949c55a --- /dev/null +++ b/test/regress/regress1/sygus/issue3654.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) |