test/regress/regress0/bug382.smt2

   1 ; EXPECT: sat
   2 ; EXPECT: ((x 0))
   3 ; EXPECT: ((x 0))
   4 ; EXPECT: (((f x) 0))
   5 ; EXPECT: (((f x) 0))
   6 (set-option :produce-models true)
   7 (set-logic QF_UFLIA)
   8 (declare-fun f (Int) Int)
   9 (declare-fun x () Int)
  10 (check-sat)
  11 (get-value (x)); returns 0
  12 (get-value (x)); returns 1 ?!
  13 (get-value ((f x))); assert-fails in EqualityEngine
  14 (get-value ((f x)))