diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-25 12:09:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-25 12:09:42 -0500 |
| commit | 91565cda11ad42082a11055514e12ddeee459460 (patch) | |
| tree | 56df21e0a0c5d0734cd40b3ce93ced2c2beac54d /test | |
| parent | 4f384b6fadd999324d83b4c4ea900de2a0e13dd7 (diff) | |
Add isParameterized function to Expr (#3303)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/concat_extract_example.sy | 22 |
2 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6dc44e314..bcae83b0a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1650,6 +1650,7 @@ set(regress_1_tests regress1/sygus/clock-inc-tuple.sy regress1/sygus/commutative-stream.sy regress1/sygus/commutative.sy + regress1/sygus/concat_extract_example.sy regress1/sygus/constant-bool-si-all.sy regress1/sygus/constant-dec-tree-bug.sy regress1/sygus/constant-ite-bv.sy diff --git a/test/regress/regress1/sygus/concat_extract_example.sy b/test/regress/regress1/sygus/concat_extract_example.sy new file mode 100644 index 000000000..7d6690816 --- /dev/null +++ b/test/regress/regress1/sygus/concat_extract_example.sy @@ -0,0 +1,22 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --lang=sygus2 +(set-logic BV) +(synth-fun f (( x (_ BitVec 32))) (_ BitVec 32) + ((BV32 (_ BitVec 32)) ( BV16 (_ BitVec 16))) + ((BV32 (_ BitVec 32) (#x00000000 #x00000001 #xFFFFFFFF + x + (bvand BV32 BV32) + (bvor BV32 BV32) + (bvnot BV32) + (concat BV16 BV16) + )) + (BV16 (_ BitVec 16) (#x0000 #x0001 #xFFFF + (bvand BV16 BV16) + (bvor BV16 BV16) + (bvnot BV16) + ((_ extract 31 16) BV32) + ((_ extract 15 0) BV32))))) +( constraint (= ( f #x0782ECAD ) #xECAD0000)) +( constraint (= ( f #xFFFF008E ) #x008E0000)) +( constraint (= ( f #x00000000 ) #x00000000)) +( check-synth ) |