title: Z3 bitvector operations
body: <p>How does one use the 'repeat' and 'rotate_left' bitvector operations?</p>
  
  <p>More generally, where can I find detailed documentation of bitvector operations in the SMT2 scripting format used by Z3?</p>
  
  <p>Everything I find seems to just go to tutorials, or broken links:<br>
  <a href="https://github.com/Z3Prover/z3/wiki/Documentation" rel="nofollow">https://github.com/Z3Prover/z3/wiki/Documentation</a><br>
  <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/old/documentation.html" rel="nofollow">http://research.microsoft.com/en-us/um/redmond/projects/z3/old/documentation.html</a></p>
  
  <p>Trying to understand "repeat", "rotate_left", and "rotate_right" by guessing has been frustating. I cannot figure out how to use them.  For example</p>
  
  <pre><code>(display (repeat #b01))
  (display (repeat #b01 3))
  (display (repeat 3))
  (display (rotate_left #b0001 2))
  </code></pre>
  
  <p>gives</p>
  
  <pre><code>"repeat expects one non-zero integer parameter"
  "repeat expects one argument"
  "operator is applied to arguments of the wrong sort"
  "rotate left expects one argument"
  </code></pre>
  
  <p>Where is the documentation?  Hoping they didn't explain because all of this is standard, I also looked at smt-lib.org but that doesn't list these details either. So frustrating.</p>