diff options
Diffstat (limited to 'test/regress/regress1/sygus/pbe_multi.sy')
| -rw-r--r-- | test/regress/regress1/sygus/pbe_multi.sy | 66 |
1 files changed, 31 insertions, 35 deletions
diff --git a/test/regress/regress1/sygus/pbe_multi.sy b/test/regress/regress1/sygus/pbe_multi.sy index 70cb6b2d2..4c588ee17 100644 --- a/test/regress/regress1/sygus/pbe_multi.sy +++ b/test/regress/regress1/sygus/pbe_multi.sy @@ -1,27 +1,25 @@ ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
-(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
-(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
-(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
-(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
-
-(synth-fun f ( (x (BitVec 64))) (BitVec 64)
-(
-
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
- (shl1 Start)
- (shr1 Start)
- (shr4 Start)
- (shr16 Start)
- (bvand Start Start)
- (bvor Start Start)
- (bvxor Start Start)
- (bvadd Start Start)
- (if0 Start Start Start)
- ))
+(define-fun shr1 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000001))
+(define-fun shr4 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000004))
+(define-fun shr16 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000010))
+(define-fun shl1 ((x (_ BitVec 64))) (_ BitVec 64) (bvshl x #x0000000000000001))
+(define-fun if0 ((x (_ BitVec 64)) (y (_ BitVec 64)) (z (_ BitVec 64))) (_ BitVec 64) (ite (= x #x0000000000000001) y z))
+
+(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)
+((Start (_ BitVec 64)))
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+ (shl1 Start)
+ (shr1 Start)
+ (shr4 Start)
+ (shr16 Start)
+ (bvand Start Start)
+ (bvor Start Start)
+ (bvxor Start Start)
+ (bvadd Start Start)
+ (if0 Start Start Start)))
)
)
@@ -37,20 +35,18 @@ (constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee))
(constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a))
-(synth-fun g ( (x (BitVec 64))) (BitVec 64)
-(
-
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
- (shl1 Start)
- (shr1 Start)
- (shr4 Start)
- (shr16 Start)
- (bvand Start Start)
- (bvor Start Start)
- (bvxor Start Start)
- (bvadd Start Start)
- (if0 Start Start Start)
- ))
+(synth-fun g ( (x (_ BitVec 64))) (_ BitVec 64)
+((Start (_ BitVec 64)))
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+ (shl1 Start)
+ (shr1 Start)
+ (shr4 Start)
+ (shr16 Start)
+ (bvand Start Start)
+ (bvor Start Start)
+ (bvxor Start Start)
+ (bvadd Start Start)
+ (if0 Start Start Start)))
)
)
|