fixup! Translate and register formula_fn

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: coord-e

src/analyze/annot_fn.rs

@@ -312,15 +312,16 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
             },
             ExprKind::Lit(lit) => match lit.node {
                 rustc_ast::LitKind::Int(i, _) => {
-                    let t = chc::Term::int(i.get() as i64);
-                    FormulaOrTerm::Term(t)
+                    let n = i64::try_from(i.get())
+                        .expect("integer literal out of i64 range in formula");
+                    FormulaOrTerm::Term(chc::Term::int(n))
                 }
                 rustc_ast::LitKind::Bool(b) => FormulaOrTerm::Literal(b),
                 _ => unimplemented!("unsupported literal in formula: {:?}", lit),
             },
             ExprKind::Path(qpath) => {
                 if let rustc_hir::def::Res::Local(hir_id) =
-                    self.typeck.qpath_res(&qpath, self.body.value.hir_id)
+                    self.typeck.qpath_res(&qpath, hir.hir_id)
                 {
                     FormulaOrTerm::Term(
                         self.env
@@ -355,6 +356,11 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
                             let t2 = self.to_term(&args[1]);
                             return FormulaOrTerm::Term(chc::Term::mut_(t1, t2));
                         }
+                        if Some(def_id) == self.def_ids.box_model_new() {
+                            assert_eq!(args.len(), 1, "Box::new takes exactly 1 argument");
+                            let t = self.to_term(&args[0]);
+                            return FormulaOrTerm::Term(chc::Term::box_(t));
+                        }
                     }
                 }
                 unimplemented!("unsupported call in formula: {:?}", func_expr)