test/regress/cli/regress0/get-value-no-evaluate.smt2

   1 ; COMMAND-LINE: -q
   2 ; SCRUBBER: sed 's/(.*//g'
   3 ; EXPECT: sat
   4 (set-logic ALL)
   5 (set-option :global-declarations true)
   6 (set-option :produce-models true)
   7 (declare-const _x29 Real)
   8 (check-sat)
   9 (get-value ((forall ((_x56 Real)) (=> (>= _x29 _x56 _x29) (>= _x29 _x56 _x29)))))