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