{"ast_node_type":"other","tokens":[{"end":42,"kind":"keyword","start":0,"text":"orig_values:"}]}
            orig_values: self.orig_values,
            uncanonicalized_goal: self.uncanonicalized_goal,
            kind: if self.encountered_overflow {