add-io-pairs-tests-sub-1

(defun g
  (x y)
  (declare (xargs :guard (and (natp x) (natp y))))
  (mv (non-exec (* 10 x)) (* 10 y)))

(defun g2
  (x)
  (declare (xargs :guard (natp x)))
  (non-exec (* 100 x)))