diff options
Diffstat (limited to 'test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy')
| -rw-r--r-- | test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy deleted file mode 100644 index abcfc2217..000000000 --- a/test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy +++ /dev/null @@ -1,32 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status - -(set-logic BV) - -(define-fun hd19 ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) - (bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m)))) - -; bvand is a duplicate -(synth-fun f ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) - ((Start (BitVec 32) ((bvand Start Start) - (bvsub Start Start) - (bvxor Start Start) - (bvor Start Start) - (bvand Start Start) - (bvshl Start Start) - (bvlshr Start Start) - (bvashr Start Start) - (bvnot Start) - (bvneg Start) - x - m - k)))) - - -(declare-var x (BitVec 32)) -(declare-var m (BitVec 32)) -(declare-var k (BitVec 32)) - -(constraint (= (hd19 x m k) (f x m k))) -(check-synth) - |