(set-option :parallel.enable true)
(set-option :model_validate true)
(declare-fun a (Int) Int)
(assert (distinct 0 (a 0)))
(check-sat-using psat)

[600] % z3 small.smt2
failed to verify: (distinct 0 (a 0))
evaluated to false
(params override_incremental true keep_cardinality_constraints true pb.solver solver xor_solver false inprocess.max 2 restart.max 5000 lookahead_simplify true retain_blocked_clauses false max_conflicts 4294967295)
(= 0 (a 0)) |-> 0
sat
(error "line 5 column 21: an invalid model was generated")
[601] % 
[601] % cat small.smt2
(set-option :parallel.enable true)
(set-option :model_validate true)
(declare-fun a (Int) Int)
(assert (distinct 0 (a 0)))
(check-sat-using psat)
[602] %