test/regress/cli/regress0/cvc-rerror-print.cvc.smt2

   1 ; EXPECT: unsat
   2 ; EXPECT: (error "Cannot get model unless after a SAT or UNKNOWN response.")
   3 (set-option :incremental false)
   4 (set-logic ALL)
   5 (set-option :produce-models true)
   6 (declare-fun x () Int)
   7 (check-sat-assuming ( (not (= x x)) ))
   8 (get-model)