diff options
Diffstat (limited to 'test/regress/regress1/sygus/once_2.sy')
-rw-r--r-- | test/regress/regress1/sygus/once_2.sy | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/once_2.sy b/test/regress/regress1/sygus/once_2.sy new file mode 100644 index 000000000..af6d56aaf --- /dev/null +++ b/test/regress/regress1/sygus/once_2.sy @@ -0,0 +1,44 @@ +; EXPECT: unsat +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic BV) + +(define-sort Stream () (_ BitVec 2)) + +(define-fun BV_ONE () Stream (_ bv1 2)) + +(define-fun + O ( (X Stream) ) Stream + (bvneg (bvand X (bvnot (bvsub X BV_ONE)))) +) + +(synth-fun op ((x Stream)) Stream + (( y_term Stream)) + (( y_term Stream ( + ( Constant Stream) + ( Variable Stream) + ( bvnot y_term ) + ( bvand y_term y_term ) + ( bvor y_term y_term ) + ( bvneg y_term ) + ( bvadd y_term y_term ) + ( bvsub y_term y_term ) + ( bvmul y_term y_term ) + ( bvudiv y_term y_term ) + ( bvurem y_term y_term ) + ( bvshl y_term y_term ) + ( bvlshr y_term y_term ) + )) +)) + +(define-fun C ((x Stream)) Bool + (= (op x) (O x)) +) + +(constraint (and +(C (_ bv0 2)) +(C (_ bv1 2)) +(C (_ bv2 2)) +(C (_ bv3 2)) +)) + +(check-synth) |