test/regress/regress0/bug548a.smt2

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