test/regress/regress0/bug480.smt2

   1 ; EXPECT: sat
   2 ; EXPECT: ((foo true) (bar false) (baz true))
   3 (set-logic QF_LIA)
   4 (set-option :produce-assignments true)
   5 (declare-fun x () Int)
   6 (declare-fun y () Int)
   7 (assert (! (or (! (= x (+ y 5)) :named foo) (! (= x (- y 5)) :named bar)) :named baz))
   8 (assert (and (> x 0) (<= y 5)))
   9 (check-sat)
  10 (get-assignment)