test/regress/regress0/bug303.smt2

   1 (set-logic QF_UFLIA)
   2 (set-info :status unsat)
   3
   4 ;; don't use a datatypes for currently focusing in uf
   5 (declare-sort list 0)
   6
   7 (declare-fun cons (Int list) list)
   8 (declare-fun nil () list)
   9
  10 ;;define length
  11 (declare-fun length (list) Int)
  12
  13 (assert (= (length nil) 0))
  14
  15 (declare-fun one_cons (list) list)
  16
  17 (assert (= (length (cons 1 nil)) (+ 1 (length nil))))
  18 (assert (= (one_cons nil) (cons 1 nil)))
  19 (assert (not (= (length (one_cons nil)) 1)))
  20
  21 (check-sat)
  22
  23 (exit)