diff options
Diffstat (limited to 'test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy')
| -rw-r--r-- | test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy new file mode 100644 index 000000000..abcfc2217 --- /dev/null +++ b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy @@ -0,0 +1,32 @@ +; 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) + |