test/regress/cli/regress0/named-expr-use.smt2

   1 (set-logic QF_LIA)
   2 (set-info :status unsat)
   3 (declare-fun x () Int)
   4 (declare-fun y () Int)
   5
   6 (assert (or (= x 5) (= x 7)))
   7 (assert (or (! (= x 5) :named foo) (= x y)))
   8
   9 (assert (= foo (= x 7)))
  10
  11 (check-sat)