test/regress/regress0/get-value-incremental.smt2

   1 ; COMMAND-LINE: --incremental
   2 ; EXPECT: sat
   3 ; EXPECT: (((f 0) 1))
   4 (set-info :smt-lib-version 2.0)
   5 (set-option :produce-models true)
   6 (set-logic QF_UFLIA)
   7
   8 (declare-fun f (Int) Int)
   9 (assert (= (f 0) 1))
  10 (check-sat)
  11 (get-value ((f 0)))
  12 ; add a "push" just to double-check that incremental mode is on
  13 (push)