diff options
Diffstat (limited to 'test/regress/regress2/sygus/multi-udiv.sy')
| -rw-r--r-- | test/regress/regress2/sygus/multi-udiv.sy | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/test/regress/regress2/sygus/multi-udiv.sy b/test/regress/regress2/sygus/multi-udiv.sy new file mode 100644 index 000000000..657417595 --- /dev/null +++ b/test/regress/regress2/sygus/multi-udiv.sy @@ -0,0 +1,42 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status + ( set-logic BV ) + ( define-fun hd05 ( ( x ( BitVec 32 ) ) ) ( BitVec 32 ) ( bvor x ( bvsub x #x00000001 ) ) ) +( synth-fun f ( ( x ( BitVec 32 ) ) ) ( BitVec 32 ) ( + (Start ( BitVec 32 ) ( #x00000001 + #x00000000 + #xffffffff + x + (bvsrem NT0 NT0) + (bvudiv NT0 NT0) + (bvsdiv NT0 NT0) + (bvurem NT0 NT0) + (bvsrem NT4 NT0) + (bvudiv NT4 NT0) + (bvurem NT4 NT0) + (bvsdiv NT4 NT0) + (bvnot NT0) + (bvneg NT0) + (bvadd NT0 NT0) + (bvor NT0 NT0) + (bvor NT4 NT0) + (bvadd NT4 NT0) +)) + (NT0 ( BitVec 32 ) ( #x00000001 + #x00000000 + #xffffffff + x +)) + (NT4 ( BitVec 32 ) ( (bvnot NT0) + (bvneg NT0) + (bvadd NT0 NT0) + (bvor NT0 NT0) + (bvsrem NT0 NT0) + (bvudiv NT0 NT0) + (bvsdiv NT0 NT0) + (bvurem NT0 NT0) +)) +)) + ( declare-var x ( BitVec 32 ) ) + ( constraint ( = ( hd05 x ) ( f x ) ) ) + ( check-synth ) |