test/regress/cli/regress0/bug548a.smt2

   1 ; EXPECT: unknown
   2 (set-logic AUFNIA)
   3 (declare-fun f (Int) Int)
   4
   5
   6 ; instantiated version : cvc4 answers sat
   7 ;(assert (= (f 1) (div 1 10)))
   8 ;(assert (= (f 11) (div 11 10)))
   9
  10 ; cvc4 answers unsat, should be "sat", cvc4 expected to timeout or answer "unknown"
  11 (assert (forall ((x Int)) (= (f x) (div x 10))))
  12
  13 (assert (= (f 1) 0))
  14 (assert (= (f 11) 1))
  15
  16 (check-sat)