diff options
Diffstat (limited to 'test/regress/regress0/sygus/Base16_1.sy')
| -rw-r--r-- | test/regress/regress0/sygus/Base16_1.sy | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/test/regress/regress0/sygus/Base16_1.sy b/test/regress/regress0/sygus/Base16_1.sy deleted file mode 100644 index b54c7688b..000000000 --- a/test/regress/regress0/sygus/Base16_1.sy +++ /dev/null @@ -1,34 +0,0 @@ -; EXPECT: unsat -; COMMAND-LINE: --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all -(set-logic BV) - -(define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l)))) - -(define-fun E ((x (BitVec 8))) (BitVec 8) (bvadd x #x41)) - -(define-fun f ((x (BitVec 8))) (BitVec 8) (bvsub x #x41)) - -(define-fun d ((x (BitVec 8))) Bool (bvule x #x3f)) - -(synth-fun D ((x (BitVec 8)) (y (BitVec 8)) ) (BitVec 8) - ((Start (BitVec 8) ( - (f Start) x y Const - (bvshl Start Start) (bvnot Start) - (bvand Start Start) - (bvxor Start Start) - (bvor Start Start) - (bvneg Start) - (bvadd Start Start) - (bvlshr Start Start) - (bvsub Start Start) - )) - (Const (BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00)) -)) - -(declare-var x (BitVec 8)) -(constraint (= x (D (E (B #x07 #x04 x) ) (E (B #x03 #x00 x)) )) ) - -; notice we don't have solution reconstruction for this -(check-synth) - - |