diff --git a/src/analyze.rs b/src/analyze.rs
index 9339b1da..19e91360 100644
--- a/src/analyze.rs
+++ b/src/analyze.rs
@@ -8,6 +8,7 @@
 
 use std::cell::RefCell;
 use std::collections::HashMap;
+use std::hash::Hash;
 use std::rc::Rc;
 
 use rustc_hir::lang_items::LangItem;
@@ -19,7 +20,7 @@ use rustc_span::Symbol;
 
 use crate::analyze;
 use crate::annot::{AnnotFormula, AnnotParser, Resolver};
-use crate::chc;
+use crate::chc::{self, ForallSortIdx};
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{self, BasicBlockType, TypeBuilder};
 use crate::rty;
@@ -190,6 +191,13 @@ impl refine::EnumDefProvider for Rc<RefCell<EnumDefs>> {
 }
 
 pub type Env = refine::Env<Rc<RefCell<EnumDefs>>>;
+pub type TypeParamMap = HashMap<TypeParam, ForallSortIdx>;
+
+#[derive(Eq, PartialEq, Hash)]
+pub enum TypeParam {
+    GenericType(DefId, u32),
+    AssocType(DefId),
+}
 
 #[derive(Debug, Clone)]
 struct DeferredFormulaFnDef<'tcx> {
@@ -217,6 +225,8 @@ pub struct Analyzer<'tcx> {
     def_ids: did_cache::DefIdCache<'tcx>,
 
     enum_defs: Rc<RefCell<EnumDefs>>,
+
+    type_params: Rc<RefCell<TypeParamMap>>,
 }
 
 impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> {
@@ -240,6 +250,7 @@ impl<'tcx> Analyzer<'tcx> {
         let system = Default::default();
         let basic_blocks = Default::default();
         let enum_defs = Default::default();
+        let type_params = Default::default();
         Self {
             tcx,
             defs,
@@ -248,6 +259,7 @@ impl<'tcx> Analyzer<'tcx> {
             basic_blocks,
             def_ids: did_cache::DefIdCache::new(tcx),
             enum_defs,
+            type_params,
         }
     }
 
@@ -281,7 +293,7 @@ impl<'tcx> Analyzer<'tcx> {
                     .iter()
                     .map(|field| {
                         let field_ty = self.tcx.type_of(field.did).instantiate_identity();
-                        TypeBuilder::new(self.tcx, self.def_ids(), def_id).build(field_ty)
+                        self.type_builder(self.def_ids(), def_id).build(field_ty)
                     })
                     .collect();
                 rty::EnumVariantDef {
@@ -380,14 +392,13 @@ impl<'tcx> Analyzer<'tcx> {
             ?mode,
             "register_deferred_def"
         );
-        self.defs.insert(
-            target_def_id,
+        self.defs.entry(target_def_id).or_insert_with(|| {
             DefTy::Deferred(DeferredDefTy {
                 local_def_id,
                 cache: Rc::new(RefCell::new(HashMap::new())),
                 mode,
-            }),
-        );
+            })
+        });
     }
 
     pub fn concrete_def_ty(&self, def_id: DefId) -> Option<&rty::RefinedType> {
@@ -401,6 +412,7 @@ impl<'tcx> Analyzer<'tcx> {
         &self,
         local_def_id: LocalDefId,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        owner_fn_id: DefId,
     ) -> Option<annot_fn::FormulaFn<'tcx>> {
         let deferred_formula_fn = self.formula_fns.get(&local_def_id)?;
 
@@ -409,9 +421,15 @@ impl<'tcx> Analyzer<'tcx> {
             return Some(formula_fn.clone());
         }
 
-        let translator = annot_fn::AnnotFnTranslator::new(self.tcx, local_def_id)
-            .with_generic_args(generic_args)
-            .with_def_id_cache(self.def_ids());
+        let translator = annot_fn::AnnotFnTranslator::new(
+            self.tcx,
+            local_def_id,
+            self.type_params.clone(),
+            self.system.clone(),
+            owner_fn_id,
+        )
+        .with_generic_args(generic_args)
+        .with_def_id_cache(self.def_ids());
         let formula_fn = translator.to_formula_fn();
         deferred_formula_fn_cache
             .borrow_mut()
@@ -425,8 +443,9 @@ impl<'tcx> Analyzer<'tcx> {
         &mut self,
         def_id: DefId,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        caller_def_id: DefId,
     ) -> Option<rty::RefinedType> {
-        let type_builder = TypeBuilder::new(self.tcx, self.def_ids(), def_id);
+        let type_builder = self.type_builder(self.def_ids(), caller_def_id);
 
         let deferred_ty = match self.defs.get(&def_id)? {
             DefTy::Concrete(rty) => {
@@ -531,8 +550,19 @@ impl<'tcx> Analyzer<'tcx> {
         &mut self,
         local_def_id: LocalDefId,
         bb: BasicBlock,
+        owner_fn_id: DefId,
     ) -> basic_block::Analyzer<'tcx, '_> {
-        basic_block::Analyzer::new(self, local_def_id, bb)
+        basic_block::Analyzer::new(self, local_def_id, bb, owner_fn_id)
+    }
+
+    pub fn type_builder(&self, def_ids: DefIdCache<'tcx>, owner_fn_id: DefId) -> TypeBuilder<'tcx> {
+        TypeBuilder::new(
+            self.tcx,
+            def_ids,
+            owner_fn_id,
+            self.type_params.clone(),
+            self.system.clone(),
+        )
     }
 
     pub fn solve(&mut self) {
@@ -626,6 +656,7 @@ impl<'tcx> Analyzer<'tcx> {
         resolver: T,
         self_type_name: Option<String>,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        owner_fn_id: DefId,
     ) -> Option<AnnotFormula<T::Output>>
     where
         T: Resolver<Output = rty::FunctionParamIdx>,
@@ -656,7 +687,9 @@ impl<'tcx> Analyzer<'tcx> {
             if require_annot.is_some() {
                 unimplemented!();
             }
-            let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else {
+            let Some(formula_fn) =
+                self.formula_fn_with_args(formula_def_id, generic_args, owner_fn_id)
+            else {
                 panic!(
                     "require annotation {:?} is not a formula function",
                     formula_def_id
@@ -675,6 +708,7 @@ impl<'tcx> Analyzer<'tcx> {
         resolver: T,
         self_type_name: Option<String>,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        owner_fn_id: DefId,
     ) -> Option<AnnotFormula<T::Output>>
     where
         T: Resolver<Output = rty::RefinedTypeVar<rty::FunctionParamIdx>>,
@@ -706,7 +740,9 @@ impl<'tcx> Analyzer<'tcx> {
             if ensure_annot.is_some() {
                 unimplemented!();
             }
-            let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else {
+            let Some(formula_fn) =
+                self.formula_fn_with_args(formula_def_id, generic_args, owner_fn_id)
+            else {
                 panic!(
                     "ensure annotation {:?} is not a formula function",
                     formula_def_id
diff --git a/src/analyze/annot_fn.rs b/src/analyze/annot_fn.rs
index aae82be4..561abb06 100644
--- a/src/analyze/annot_fn.rs
+++ b/src/analyze/annot_fn.rs
@@ -1,13 +1,18 @@
+use std::cell::RefCell;
 use std::collections::HashMap;
+use std::rc::Rc;
 
 use pretty::{termcolor, Pretty};
-use rustc_hir::{def_id::LocalDefId, HirId};
+use rustc_hir::{
+    def_id::{DefId, LocalDefId},
+    HirId,
+};
 use rustc_index::IndexVec;
-use rustc_middle::ty::{self as mir_ty, TyCtxt};
+use rustc_middle::ty::{self as mir_ty, TyCtxt, TypeFoldable};
 
-use crate::analyze::{self, did_cache::DefIdCache};
+use crate::analyze::{self, did_cache::DefIdCache, TypeParamMap};
 use crate::annot::AnnotFormula;
-use crate::chc;
+use crate::chc::{self, System};
 use crate::refine::{self, TypeBuilder};
 use crate::rty;
 
@@ -137,15 +142,30 @@ pub struct AnnotFnTranslator<'tcx> {
     def_ids: DefIdCache<'tcx>,
     type_builder: TypeBuilder<'tcx>,
     env: HashMap<HirId, chc::Term<rty::FunctionParamIdx>>,
+
+    type_params: Rc<RefCell<TypeParamMap>>,
+    system: Rc<RefCell<System>>,
 }
 
 impl<'tcx> AnnotFnTranslator<'tcx> {
-    pub fn new(tcx: TyCtxt<'tcx>, local_def_id: LocalDefId) -> Self {
+    pub fn new(
+        tcx: TyCtxt<'tcx>,
+        local_def_id: LocalDefId,
+        type_params: Rc<RefCell<TypeParamMap>>,
+        system: Rc<RefCell<System>>,
+        owner_fn_id: DefId,
+    ) -> Self {
         let body = tcx.hir_body_owned_by(local_def_id);
         let generic_args = tcx.mk_args(&[]);
         let typeck = tcx.typeck(local_def_id);
         let def_ids = DefIdCache::new(tcx);
-        let type_builder = TypeBuilder::new(tcx, def_ids.clone(), local_def_id.to_def_id());
+        let type_builder = TypeBuilder::new(
+            tcx,
+            def_ids.clone(),
+            owner_fn_id,
+            type_params.clone(),
+            system.clone(),
+        );
         let mut translator = Self {
             tcx,
             local_def_id,
@@ -155,6 +175,8 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
             def_ids,
             type_builder,
             env: HashMap::default(),
+            type_params,
+            system,
         };
         translator.build_env_from_params();
         translator
@@ -171,6 +193,8 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
             self.tcx,
             self.def_ids.clone(),
             self.local_def_id.to_def_id(),
+            self.type_params.clone(),
+            self.system.clone(),
         );
         self
     }
@@ -204,29 +228,48 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
         }
     }
 
+    fn instantiate_generics<T>(
+        &self,
+        ty: T,
+        generic_args: mir_ty::GenericArgsRef<'tcx>,
+    ) -> Option<T>
+    where
+        T: TypeFoldable<TyCtxt<'tcx>>,
+    {
+        if !self.generic_args.is_empty() {
+            Some(mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, generic_args))
+        } else {
+            None
+        }
+    }
+
     fn expr_ty(&self, expr: &'tcx rustc_hir::Expr<'tcx>) -> mir_ty::Ty<'tcx> {
         let ty = self.typeck.expr_ty(expr);
-        let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args);
+        let instantiated = self
+            .instantiate_generics(ty, self.generic_args)
+            .unwrap_or(ty);
         let typing_env = mir_ty::TypingEnv::fully_monomorphized();
         self.tcx.normalize_erasing_regions(typing_env, instantiated)
     }
 
     fn pat_ty(&self, pat: &'tcx rustc_hir::Pat<'tcx>) -> mir_ty::Ty<'tcx> {
         let ty = self.typeck.pat_ty(pat);
-        let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args);
+        let instantiated = self
+            .instantiate_generics(ty, self.generic_args)
+            .unwrap_or(ty);
         let typing_env = mir_ty::TypingEnv::fully_monomorphized();
         self.tcx.normalize_erasing_regions(typing_env, instantiated)
     }
 
     pub fn to_formula_fn(&self) -> FormulaFn<'tcx> {
         let formula = self.to_formula(self.body.value);
-        let params = self
-            .tcx
-            .fn_sig(self.local_def_id.to_def_id())
-            .instantiate(self.tcx, self.generic_args)
-            .skip_binder()
-            .inputs()
-            .to_vec();
+        let fn_sig = self.tcx.fn_sig(self.local_def_id.to_def_id());
+        let binder = if self.generic_args.is_empty() {
+            fn_sig.skip_binder()
+        } else {
+            fn_sig.instantiate(self.tcx, self.generic_args)
+        };
+        let params = binder.skip_binder().inputs().to_vec();
         FormulaFn {
             params: IndexVec::from_raw(params),
             formula,
@@ -495,8 +538,12 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
                                 outer_generic_args = ?self.generic_args,
                                 "resolving predicate call in formula"
                             );
-                            let generic_args = mir_ty::EarlyBinder::bind(generic_args)
-                                .instantiate(self.tcx, self.generic_args);
+                            let (mut is_unresolved_args, generic_args) =
+                                match self.instantiate_generics(generic_args, self.generic_args) {
+                                    Some(args) => (false, args),
+                                    None => (true, generic_args),
+                                };
+
                             let instance = mir_ty::Instance::try_resolve(
                                 self.tcx,
                                 typing_env,
@@ -507,11 +554,30 @@ impl<'tcx> AnnotFnTranslator<'tcx> {
                             let pred_def_id = if let Some(instance) = instance {
                                 instance.def_id()
                             } else {
+                                is_unresolved_args = true;
                                 def_id
                             };
-                            let pred = refine::user_defined_pred(self.tcx, pred_def_id);
+
+                            let typeck_results = self.tcx.typeck(self.local_def_id);
+                            let pred = if is_unresolved_args {
+                                let pred = refine::forall_pred(self.tcx, pred_def_id);
+                                let sig = args
+                                    .iter()
+                                    .map(|e| {
+                                        let ty = typeck_results.expr_ty(e);
+                                        self.type_builder.build(ty).to_sort()
+                                    })
+                                    .collect();
+                                self.system
+                                    .borrow_mut()
+                                    .register_forall_pred(pred.clone(), sig);
+                                pred.into()
+                            } else {
+                                refine::user_defined_pred(self.tcx, pred_def_id).into()
+                            };
+                            tracing::debug!("resolved predicate call in formula: {:?}", pred);
                             let arg_terms = args.iter().map(|e| self.to_term(e)).collect();
-                            let atom = chc::Atom::new(pred.into(), arg_terms);
+                            let atom = chc::Atom::new(pred, arg_terms);
                             return FormulaOrTerm::Formula(chc::Formula::Atom(atom));
                         }
                     }
diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs
index 15d70033..1b0949dd 100644
--- a/src/analyze/basic_block.rs
+++ b/src/analyze/basic_block.rs
@@ -636,7 +636,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         def_id: DefId,
         args: mir_ty::GenericArgsRef<'tcx>,
     ) -> rty::Type<rty::Closed> {
-        if let Some(def_ty) = self.ctx.def_ty_with_args(def_id, args) {
+        let caller_def_id = self.type_builder.owner_fn_id;
+        if let Some(def_ty) = self.ctx.def_ty_with_args(def_id, args, caller_def_id) {
             return def_ty.ty;
         }
 
@@ -648,7 +649,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             );
         }
         tracing::info!(?def_id, ?resolved_def_id, ?resolved_args, "resolved");
-        let Some(def_ty) = self.ctx.def_ty_with_args(resolved_def_id, resolved_args) else {
+        let Some(def_ty) = self
+            .ctx
+            .def_ty_with_args(resolved_def_id, resolved_args, caller_def_id)
+        else {
             panic!(
                 "unknown def (resolved): {:?}, args: {:?}",
                 resolved_def_id, resolved_args
@@ -1166,6 +1170,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         ctx: &'ctx mut analyze::Analyzer<'tcx>,
         local_def_id: LocalDefId,
         basic_block: BasicBlock,
+        owner_fn_id: DefId,
     ) -> Self {
         let tcx = ctx.tcx;
         let drop_points = DropPoints::default();
@@ -1173,7 +1178,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let env = ctx.new_env();
         let local_decls = body.local_decls.clone();
         let prophecy_vars = Default::default();
-        let type_builder = TypeBuilder::new(tcx, ctx.def_ids(), local_def_id.to_def_id());
+        let type_builder = ctx.type_builder(ctx.def_ids(), owner_fn_id);
         Self {
             ctx,
             tcx,
diff --git a/src/analyze/crate_.rs b/src/analyze/crate_.rs
index c85038fa..58bd309e 100644
--- a/src/analyze/crate_.rs
+++ b/src/analyze/crate_.rs
@@ -8,7 +8,7 @@ use rustc_span::def_id::LocalDefId;
 
 use crate::analyze;
 use crate::chc;
-use crate::rty::{self, ClauseBuilderExt as _};
+use crate::rty::ClauseBuilderExt as _;
 
 /// An implementation of local crate analysis.
 ///
@@ -69,8 +69,6 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 
     #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(local_def_id)))]
     fn refine_fn_def(&mut self, local_def_id: LocalDefId) {
-        let sig = self.ctx.fn_sig(local_def_id.to_def_id());
-
         let mut analyzer = self.ctx.local_def_analyzer(local_def_id);
 
         if analyzer.is_annotated_as_trusted() {
@@ -113,24 +111,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             }
         }
 
-        let target_def_id = if analyzer.is_annotated_as_extern_spec_fn() {
-            analyzer.extern_spec_fn_target_def_id()
-        } else {
-            local_def_id.to_def_id()
-        };
-
-        use mir_ty::TypeVisitableExt as _;
-        if sig.has_param() {
-            if self.skip_analysis.contains(&local_def_id) {
-                self.ctx
-                    .register_deferred_def_without_analysis(target_def_id, local_def_id);
-            } else {
-                self.ctx.register_deferred_def(local_def_id);
-            }
-        } else {
-            let expected = analyzer.expected_ty();
-            self.ctx.register_def(target_def_id, expected);
-        }
+        let owner_fn_id = analyzer.owner_fn_id;
+        let expected = analyzer.expected_ty();
+        self.ctx.register_def(owner_fn_id, expected);
     }
 
     fn analyze_local_defs(&mut self) {
@@ -139,25 +122,19 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 continue;
             };
             if self.skip_analysis.contains(local_def_id) {
+                tracing::debug!("this is marked as skip analysis: {:?}", local_def_id);
                 continue;
             }
 
             let Some(expected) = self.ctx.concrete_def_ty(local_def_id.to_def_id()) else {
                 // when the local_def_id is deferred it would be skipped
+                tracing::debug!("this is marked as deferred type: {:?}", local_def_id);
                 continue;
             };
 
             // check polymorphic function def by replacing type params with some opaque type
             // (and this is no-op if the function is mono)
-            let mut expected = expected.clone();
-            let subst = rty::TypeParamSubst::new(
-                expected
-                    .free_ty_params()
-                    .into_iter()
-                    .map(|ty_param| (ty_param, rty::RefinedType::unrefined(rty::Type::int())))
-                    .collect(),
-            );
-            expected.subst_ty_params(&subst);
+            let expected = expected.clone();
             let generic_args = self.placeholder_generic_args(*local_def_id);
             self.ctx
                 .local_def_analyzer(*local_def_id)
@@ -196,12 +173,17 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             let arg = match param.kind {
                 mir_ty::GenericParamDefKind::Type { .. } => {
                     if constrained_params.contains(&param.index) {
-                        panic!(
-                            "unable to check generic function with constrained type parameter: {}",
-                            self.tcx.def_path_str(local_def_id)
+                        let new_param =
+                            mir_ty::Ty::new_param(self.tcx, param.index, param.name).into();
+                        tracing::debug!(
+                            "replace the cosnstrained param {:#?} with the new param {:#?}.",
+                            param,
+                            new_param
                         );
+                        new_param
+                    } else {
+                        self.tcx.types.i32.into()
                     }
-                    self.tcx.types.i32.into()
                 }
                 mir_ty::GenericParamDefKind::Const { .. } => {
                     unimplemented!()
diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs
index be309448..de10fe8c 100644
--- a/src/analyze/local_def.rs
+++ b/src/analyze/local_def.rs
@@ -37,6 +37,82 @@ fn stmt_str_literal(stmt: &rustc_hir::Stmt) -> Option<String> {
     }
 }
 
+fn is_annotated_as_extern_spec_fn_impl(tcx: &TyCtxt, local_def_id: &LocalDefId) -> bool {
+    tcx.get_attrs_by_path(
+        local_def_id.to_def_id(),
+        &analyze::annot::extern_spec_fn_path(),
+    )
+    .next()
+    .is_some()
+}
+
+/// Extract the target DefId from `#[thrust::extern_spec_fn]` function.
+///
+/// The target is identified as the tail call expression (last expression without
+/// semicolon) in the function body block.
+fn extern_spec_fn_target_def_id_impl<'tcx>(
+    tcx: &TyCtxt<'tcx>,
+    local_def_id: &LocalDefId,
+    mir_body: &Body<'tcx>,
+) -> DefId {
+    let hir_node = tcx.hir_node_by_def_id(*local_def_id);
+    let hir_body_id = match hir_node {
+        rustc_hir::Node::Item(item) => {
+            let rustc_hir::ItemKind::Fn { body: body_id, .. } = item.kind else {
+                panic!("extern_spec_fn must be a function");
+            };
+            body_id
+        }
+        rustc_hir::Node::ImplItem(impl_item) => {
+            let rustc_hir::ImplItemKind::Fn(_, body_id) = impl_item.kind else {
+                panic!("extern_spec_fn must be a function");
+            };
+            body_id
+        }
+        rustc_hir::Node::TraitItem(trait_item) => {
+            let rustc_hir::TraitItemKind::Fn(_, rustc_hir::TraitFn::Provided(body_id)) =
+                trait_item.kind
+            else {
+                panic!("extern_spec_fn must be a function with a body");
+            };
+            body_id
+        }
+        _ => panic!("extern_spec_fn must be a function item or impl item"),
+    };
+
+    let hir_body = tcx.hir_body(hir_body_id);
+
+    // The body is a block; the tail expression is the function call to the target.
+    let rustc_hir::ExprKind::Block(block, _) = &hir_body.value.kind else {
+        panic!("extern_spec_fn body must be a block");
+    };
+    let tail_expr = block
+        .expr
+        .expect("extern_spec_fn block must end with a tail call expression");
+
+    let rustc_hir::ExprKind::Call(func_expr, _) = &tail_expr.kind else {
+        panic!("extern_spec_fn tail expression must be a function call");
+    };
+    let rustc_hir::ExprKind::Path(qpath) = &func_expr.kind else {
+        panic!("extern_spec_fn call must be a path expression");
+    };
+
+    let typeck_result = tcx.typeck(local_def_id);
+    let hir_id = func_expr.hir_id;
+    let rustc_hir::def::Res::Def(_, def_id) = typeck_result.qpath_res(qpath, hir_id) else {
+        panic!("extern_spec_fn call must resolve to a definition");
+    };
+
+    let args = typeck_result.node_args(hir_id);
+    let typing_env = mir_body.typing_env(*tcx);
+    let instance = mir_ty::Instance::try_resolve(*tcx, typing_env, def_id, args).unwrap();
+    if let Some(instance) = instance {
+        instance.def_id()
+    } else {
+        def_id
+    }
+}
+
 /// An implementation of the typing of local definitions.
 ///
 /// The current implementation only applies to function definitions. The entry point is
@@ -46,6 +122,7 @@ pub struct Analyzer<'tcx, 'ctx> {
     tcx: TyCtxt<'tcx>,
 
     local_def_id: LocalDefId,
+    pub owner_fn_id: DefId,
 
     body: Body<'tcx>,
     /// to substitute HIR types during translation in [`crate::analyze::annot_fn`]
@@ -201,13 +278,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     }
 
     pub fn is_annotated_as_extern_spec_fn(&self) -> bool {
-        self.tcx
-            .get_attrs_by_path(
-                self.local_def_id.to_def_id(),
-                &analyze::annot::extern_spec_fn_path(),
-            )
-            .next()
-            .is_some()
+        is_annotated_as_extern_spec_fn_impl(&self.tcx, &self.local_def_id)
     }
 
     pub fn is_annotated_as_predicate(&self) -> bool {
@@ -318,7 +389,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             .associated_item(self.local_def_id.to_def_id())
             .trait_item_def_id
             .unwrap();
-        self.ctx.def_ty_with_args(trait_item_did, trait_ref.args)
+        self.ctx
+            .def_ty_with_args(trait_item_did, trait_ref.args, trait_ref.def_id)
     }
 
     // Note that we do not expect predicate variables to be generated here
@@ -358,6 +430,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             &param_resolver,
             self_type_name.clone(),
             self.generic_args,
+            self.owner_fn_id,
         );
 
         let mut ensure_annot = self.ctx.extract_ensure_annot(
@@ -365,6 +438,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             &result_param_resolver,
             self_type_name.clone(),
             self.generic_args,
+            self.owner_fn_id,
         );
 
         if let Some(trait_item_id) = self.local_trait_item_id() {
@@ -374,12 +448,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 &param_resolver,
                 self_type_name.clone(),
                 self.generic_args,
+                self.owner_fn_id,
             );
             let trait_ensure_annot = self.ctx.extract_ensure_annot(
                 trait_item_id,
                 &result_param_resolver,
                 self_type_name.clone(),
                 self.generic_args,
+                self.owner_fn_id,
             );
 
             assert!(require_annot.is_none() || trait_require_annot.is_none());
@@ -447,62 +523,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     /// The target is identified as the tail call expression (last expression without
     /// semicolon) in the function body block.
     pub fn extern_spec_fn_target_def_id(&self) -> DefId {
-        let node = self.tcx.hir_node_by_def_id(self.local_def_id);
-        let body_id = match node {
-            rustc_hir::Node::Item(item) => {
-                let rustc_hir::ItemKind::Fn { body: body_id, .. } = item.kind else {
-                    panic!("extern_spec_fn must be a function");
-                };
-                body_id
-            }
-            rustc_hir::Node::ImplItem(impl_item) => {
-                let rustc_hir::ImplItemKind::Fn(_, body_id) = impl_item.kind else {
-                    panic!("extern_spec_fn must be a function");
-                };
-                body_id
-            }
-            rustc_hir::Node::TraitItem(trait_item) => {
-                let rustc_hir::TraitItemKind::Fn(_, rustc_hir::TraitFn::Provided(body_id)) =
-                    trait_item.kind
-                else {
-                    panic!("extern_spec_fn must be a function with a body");
-                };
-                body_id
-            }
-            _ => panic!("extern_spec_fn must be a function item or impl item"),
-        };
-
-        let body = self.tcx.hir_body(body_id);
-
-        // The body is a block; the tail expression is the function call to the target.
-        let rustc_hir::ExprKind::Block(block, _) = &body.value.kind else {
-            panic!("extern_spec_fn body must be a block");
-        };
-        let tail_expr = block
-            .expr
-            .expect("extern_spec_fn block must end with a tail call expression");
-
-        let rustc_hir::ExprKind::Call(func_expr, _) = &tail_expr.kind else {
-            panic!("extern_spec_fn tail expression must be a function call");
-        };
-        let rustc_hir::ExprKind::Path(qpath) = &func_expr.kind else {
-            panic!("extern_spec_fn call must be a path expression");
-        };
-
-        let typeck_result = self.tcx.typeck(self.local_def_id);
-        let hir_id = func_expr.hir_id;
-        let rustc_hir::def::Res::Def(_, def_id) = typeck_result.qpath_res(qpath, hir_id) else {
-            panic!("extern_spec_fn call must resolve to a definition");
-        };
-
-        let args = typeck_result.node_args(hir_id);
-        let typing_env = self.body.typing_env(self.tcx);
-        let instance = mir_ty::Instance::try_resolve(self.tcx, typing_env, def_id, args).unwrap();
-        if let Some(instance) = instance {
-            instance.def_id()
-        } else {
-            def_id
-        }
+        extern_spec_fn_target_def_id_impl(&self.tcx, &self.local_def_id, &self.body)
     }
 
     fn is_mut_param(&self, param_idx: rty::FunctionParamIdx) -> bool {
@@ -865,7 +886,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             let rty = self.ctx.basic_block_ty(self.local_def_id, bb).clone();
             let drop_points = self.drop_points[&bb].clone();
             self.ctx
-                .basic_block_analyzer(self.local_def_id, bb)
+                .basic_block_analyzer(self.local_def_id, bb, self.body.source.def_id())
                 .body(self.body.clone())
                 .drop_points(drop_points)
                 .run(&rty);
@@ -973,12 +994,18 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let tcx = ctx.tcx;
         let body = tcx.optimized_mir(local_def_id.to_def_id()).clone();
         let drop_points = Default::default();
-        let type_builder = TypeBuilder::new(tcx, ctx.def_ids(), local_def_id.to_def_id());
+        let owner_fn_id = if is_annotated_as_extern_spec_fn_impl(&tcx, &local_def_id) {
+            extern_spec_fn_target_def_id_impl(&tcx, &local_def_id, &body)
+        } else {
+            local_def_id.to_def_id()
+        };
+        let type_builder = ctx.type_builder(ctx.def_ids(), owner_fn_id);
         let generic_args = tcx.mk_args(&[]);
         Self {
             ctx,
             tcx,
             local_def_id,
+            owner_fn_id,
             body,
             generic_args,
             drop_points,
diff --git a/src/chc.rs b/src/chc.rs
index 58166391..a07c62c8 100644
--- a/src/chc.rs
+++ b/src/chc.rs
@@ -1,5 +1,7 @@
 //! A multi-sorted CHC system with tuples.
 
+use std::collections::HashMap;
+
 use pretty::{termcolor, Pretty};
 use rustc_index::IndexVec;
 
@@ -84,6 +86,45 @@ impl DatatypeSort {
     }
 }
 
+rustc_index::newtype_index! {
+    /// An index representing sort-level variable.
+    ///
+    /// We manage sort-level variables using indices that are unique in the whole CHC system.
+    /// [`System`] contains `Vec<ForallSortIdx>` that manages the indices of the variables.
+    #[orderable]
+    #[debug_format = "a{}"]
+    pub struct ForallSortIdx { }
+}
+
+impl Default for ForallSortIdx {
+    fn default() -> Self {
+        0_usize.into()
+    }
+}
+
+impl std::fmt::Display for ForallSortIdx {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        write!(f, "a{}", self.index())
+    }
+}
+
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ForallSortIdx
+where
+    D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
+{
+    fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
+        allocator
+            .as_string(self)
+            .annotate(ForallSortIdx::color_spec())
+    }
+}
+
+impl ForallSortIdx {
+    fn color_spec() -> termcolor::ColorSpec {
+        termcolor::ColorSpec::new()
+    }
+}
+
 /// A sort is the type of a logical term.
 #[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
 pub enum Sort {
@@ -97,6 +138,7 @@ pub enum Sort {
     Tuple(Vec<Sort>),
     Array(Box<Sort>, Box<Sort>),
     Datatype(DatatypeSort),
+    Forall(ForallSortIdx),
 }
 
 impl From<DatatypeSort> for Sort {
@@ -154,6 +196,7 @@ where
                 }
             }
             Sort::Datatype(sort) => sort.pretty(allocator),
+            Sort::Forall(idx) => idx.pretty(allocator),
         }
     }
 }
@@ -180,7 +223,12 @@ impl Sort {
     fn walk_impl<'a, 'b>(&'a self, mut f: Box<dyn FnMut(&'a Sort) + 'b>) {
         f(self);
         match self {
-            Sort::Null | Sort::Int | Sort::Bool | Sort::String | Sort::Param(_) => {}
+            Sort::Null
+            | Sort::Int
+            | Sort::Bool
+            | Sort::String
+            | Sort::Param(_)
+            | Sort::Forall(_) => {}
             Sort::Box(s) | Sort::Mut(s) => s.walk(Box::new(&mut f)),
             Sort::Tuple(ss) => {
                 for s in ss {
@@ -261,6 +309,10 @@ impl Sort {
         Sort::Datatype(DatatypeSort { symbol, args })
     }
 
+    pub fn forall(index: ForallSortIdx) -> Self {
+        Sort::Forall(index)
+    }
+
     pub fn into_datatype(self) -> Option<DatatypeSort> {
         match self {
             Sort::Datatype(sort) => Some(sort),
@@ -994,6 +1046,32 @@ impl UserDefinedPred {
     }
 }
 
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub struct ForallPred {
+    inner: String,
+}
+
+impl std::fmt::Display for ForallPred {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        self.inner.fmt(f)
+    }
+}
+
+impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ForallPred
+where
+    D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
+{
+    fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
+        allocator.text(self.inner.clone())
+    }
+}
+
+impl ForallPred {
+    pub fn new(inner: String) -> Self {
+        Self { inner }
+    }
+}
+
 /// A predicate.
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Pred {
@@ -1001,6 +1079,7 @@ pub enum Pred {
     Var(PredVarId),
     Matcher(MatcherPred),
     UserDefined(UserDefinedPred),
+    ForallPred(ForallPred),
 }
 
 impl std::fmt::Display for Pred {
@@ -1010,6 +1089,7 @@ impl std::fmt::Display for Pred {
             Pred::Var(p) => p.fmt(f),
             Pred::Matcher(p) => p.fmt(f),
             Pred::UserDefined(p) => p.fmt(f),
+            Pred::ForallPred(p) => p.fmt(f),
         }
     }
 }
@@ -1025,6 +1105,7 @@ where
             Pred::Var(p) => p.pretty(allocator),
             Pred::Matcher(p) => p.pretty(allocator),
             Pred::UserDefined(p) => p.pretty(allocator),
+            Pred::ForallPred(p) => p.pretty(allocator),
         }
     }
 }
@@ -1053,6 +1134,12 @@ impl From<UserDefinedPred> for Pred {
     }
 }
 
+impl From<ForallPred> for Pred {
+    fn from(p: ForallPred) -> Self {
+        Pred::ForallPred(p)
+    }
+}
+
 impl Pred {
     pub fn name(&self) -> std::borrow::Cow<'static, str> {
         match self {
@@ -1060,6 +1147,7 @@ impl Pred {
             Pred::Var(p) => p.to_string().into(),
             Pred::Matcher(p) => p.name().into(),
             Pred::UserDefined(p) => p.to_string().into(),
+            Pred::ForallPred(p) => p.to_string().into(),
         }
     }
 
@@ -1069,6 +1157,7 @@ impl Pred {
             Pred::Var(_) => false,
             Pred::Matcher(_) => false,
             Pred::UserDefined(_) => false,
+            Pred::ForallPred(_) => false,
         }
     }
 
@@ -1078,6 +1167,7 @@ impl Pred {
             Pred::Var(_) => false,
             Pred::Matcher(_) => false,
             Pred::UserDefined(_) => false,
+            Pred::ForallPred(_) => false,
         }
     }
 
@@ -1087,6 +1177,7 @@ impl Pred {
             Pred::Var(_) => false,
             Pred::Matcher(_) => false,
             Pred::UserDefined(_) => false,
+            Pred::ForallPred(_) => false,
         }
     }
 
@@ -1096,6 +1187,7 @@ impl Pred {
             Pred::Var(_) => false,
             Pred::Matcher(_) => false,
             Pred::UserDefined(_) => false,
+            Pred::ForallPred(_) => false,
         }
     }
 }
@@ -1783,6 +1875,9 @@ pub struct System {
     pub user_defined_pred_defs: Vec<UserDefinedPredDef>,
     pub clauses: IndexVec<ClauseId, Clause>,
     pub pred_vars: IndexVec<PredVarId, PredVarDef>,
+    pub forall_sorts: Vec<ForallSortIdx>,
+    pub num_forall_sort_idx: ForallSortIdx,
+    forall_pred_vars: HashMap<ForallPred, PredSig>,
 }
 
 impl System {
@@ -1790,6 +1885,17 @@ impl System {
         self.pred_vars.push(PredVarDef { sig, debug_info })
     }
 
+    pub fn register_forall_pred(&mut self, pred: ForallPred, sig: PredSig) {
+        self.forall_pred_vars.entry(pred).or_insert(sig);
+    }
+
+    pub fn new_forall_sort(&mut self) -> ForallSortIdx {
+        let new_idx = self.num_forall_sort_idx;
+        self.num_forall_sort_idx += 1;
+        self.forall_sorts.push(new_idx);
+        new_idx
+    }
+
     pub fn push_raw_command(&mut self, raw_command: RawCommand) {
         self.raw_commands.push(raw_command)
     }
diff --git a/src/chc/format_context.rs b/src/chc/format_context.rs
index 94548274..86895e02 100644
--- a/src/chc/format_context.rs
+++ b/src/chc/format_context.rs
@@ -87,6 +87,7 @@ impl<'a> std::fmt::Display for SortSymbol<'a> {
                 write!(f, "Array{}", SortSymbols::new(&[*s1.clone(), *s2.clone()]))
             }
             chc::Sort::Datatype(s) => write!(f, "{}{}", s.symbol, SortSymbols::new(&s.args)),
+            chc::Sort::Forall(i) => write!(f, "{}", i),
         }
     }
 }
diff --git a/src/chc/smtlib2.rs b/src/chc/smtlib2.rs
index e8886ed6..aab762bf 100644
--- a/src/chc/smtlib2.rs
+++ b/src/chc/smtlib2.rs
@@ -589,6 +589,34 @@ impl<'ctx, 'a> UserDefinedPredDef<'ctx, 'a> {
         Self { ctx, inner }
     }
 }
+
+pub struct ForallPredDef<'ctx, 'a> {
+    ctx: &'ctx FormatContext,
+    symbol: &'a chc::ForallPred,
+    sig: &'a chc::PredSig,
+}
+
+impl<'ctx, 'a> std::fmt::Display for ForallPredDef<'ctx, 'a> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let params = List::closed(self.sig.iter().map(|sort| self.ctx.fmt_sort(sort)));
+        write!(
+            f,
+            "(declare-forall-fun {name} {params} Bool)",
+            name = self.symbol,
+        )
+    }
+}
+
+impl<'ctx, 'a> ForallPredDef<'ctx, 'a> {
+    pub fn new(
+        ctx: &'ctx FormatContext,
+        symbol: &'a chc::ForallPred,
+        sig: &'a chc::PredSig,
+    ) -> Self {
+        Self { ctx, symbol, sig }
+    }
+}
+
 /// A wrapper around a [`chc::System`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct System<'a> {
@@ -600,6 +628,14 @@ impl<'a> std::fmt::Display for System<'a> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         writeln!(f, "(set-logic HORN)\n")?;
 
+        for forall_sort_idx in &self.inner.forall_sorts {
+            writeln!(f, "(declare-forall-sort {})\n", forall_sort_idx)?;
+        }
+
+        for (symbol, sig) in &self.inner.forall_pred_vars {
+            writeln!(f, "{}\n", ForallPredDef::new(&self.ctx, symbol, sig))?;
+        }
+
         writeln!(f, "{}\n", Datatypes::new(&self.ctx, self.ctx.datatypes()))?;
         for datatype in self.ctx.datatypes() {
             writeln!(f, "{}", DatatypeDiscrFun::new(&self.ctx, datatype))?;
diff --git a/src/chc/unbox.rs b/src/chc/unbox.rs
index b3b24d52..3f856e48 100644
--- a/src/chc/unbox.rs
+++ b/src/chc/unbox.rs
@@ -43,6 +43,7 @@ fn unbox_pred(pred: Pred) -> Pred {
         Pred::Var(pred) => Pred::Var(pred),
         Pred::Matcher(pred) => unbox_matcher_pred(pred),
         Pred::UserDefined(pred) => Pred::UserDefined(pred),
+        Pred::ForallPred(pred) => Pred::ForallPred(pred),
     }
 }
 
@@ -72,6 +73,7 @@ fn unbox_sort(sort: Sort) -> Sort {
         Sort::Tuple(sorts) => Sort::Tuple(sorts.into_iter().map(unbox_sort).collect()),
         Sort::Array(s1, s2) => Sort::Array(Box::new(unbox_sort(*s1)), Box::new(unbox_sort(*s2))),
         Sort::Datatype(sort) => Sort::Datatype(unbox_datatype_sort(sort)),
+        Sort::Forall(i) => Sort::Forall(i),
     }
 }
 
@@ -162,6 +164,11 @@ fn unbox_user_defined_pred_def(user_defined_pred_def: UserDefinedPredDef) -> Use
     UserDefinedPredDef { symbol, sig, body }
 }
 
+fn unbox_forall_pred_var_def((pred, sig): (ForallPred, PredSig)) -> (ForallPred, PredSig) {
+    let sig = sig.into_iter().map(unbox_sort).collect();
+    (pred, sig)
+}
+
 /// Remove all `Box` sorts and `Box`/`BoxCurrent` terms from the system.
 ///
 /// The box values in Thrust represent an owned pointer, but are logically equivalent to the inner type.
@@ -174,6 +181,9 @@ pub fn unbox(system: System) -> System {
         user_defined_pred_defs,
         clauses,
         pred_vars,
+        forall_sorts,
+        num_forall_sort_idx,
+        forall_pred_vars,
     } = system;
     let datatypes = datatypes.into_iter().map(unbox_datatype).collect();
     let clauses = clauses.into_iter().map(unbox_clause).collect();
@@ -182,11 +192,18 @@ pub fn unbox(system: System) -> System {
         .into_iter()
         .map(unbox_user_defined_pred_def)
         .collect();
+    let forall_pred_vars = forall_pred_vars
+        .into_iter()
+        .map(unbox_forall_pred_var_def)
+        .collect();
     System {
         raw_commands,
         datatypes,
         user_defined_pred_defs,
         clauses,
         pred_vars,
+        forall_sorts,
+        num_forall_sort_idx,
+        forall_pred_vars,
     }
 }
diff --git a/src/refine.rs b/src/refine.rs
index 60e5ad6d..1ff1291b 100644
--- a/src/refine.rs
+++ b/src/refine.rs
@@ -18,15 +18,16 @@ pub use env::{
     Assumption, EnumDefProvider, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, Var,
 };
 
-use crate::chc::{DatatypeSymbol, UserDefinedPred};
+use crate::chc::{DatatypeSymbol, ForallPred, UserDefinedPred};
 use rustc_middle::ty as mir_ty;
 use rustc_span::def_id::DefId;
 
-fn stable_def_id_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> String {
+fn stable_def_id_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId, prefix: &str) -> String {
     let hash = tcx.def_path_hash(did);
     let path = tcx.def_path(did);
     if let Some(name) = path.data.last().and_then(|d| d.data.get_opt_name()) {
-        format!("{}_{}", name, hash.0.to_hex())
+        tracing::debug!("stable_def_id_symbol: name={}", name);
+        format!("{}_{}_{}", prefix, name, hash.0.to_hex())
     } else {
         hash.0.to_hex()
     }
@@ -37,5 +38,9 @@ pub fn datatype_symbol(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> DatatypeSymbol {
 }
 
 pub fn user_defined_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> UserDefinedPred {
-    UserDefinedPred::new(stable_def_id_symbol(tcx, did))
+    UserDefinedPred::new(stable_def_id_symbol(tcx, did, "p"))
+}
+
+pub fn forall_pred(tcx: mir_ty::TyCtxt<'_>, did: DefId) -> ForallPred {
+    ForallPred::new(stable_def_id_symbol(tcx, did, "q"))
 }
diff --git a/src/refine/template.rs b/src/refine/template.rs
index a29d76d8..68cd4b58 100644
--- a/src/refine/template.rs
+++ b/src/refine/template.rs
@@ -1,4 +1,6 @@
+use std::cell::RefCell;
 use std::collections::HashMap;
+use std::rc::Rc;
 
 use rustc_index::IndexVec;
 use rustc_middle::mir::{Local, Mutability};
@@ -6,7 +8,7 @@ use rustc_middle::ty as mir_ty;
 use rustc_span::def_id::DefId;
 
 use super::basic_block::BasicBlockType;
-use crate::analyze::DefIdCache;
+use crate::analyze::{DefIdCache, TypeParam, TypeParamMap};
 use crate::chc;
 use crate::refine;
 use crate::rty;
@@ -71,17 +73,26 @@ where
 pub struct TypeBuilder<'tcx> {
     tcx: mir_ty::TyCtxt<'tcx>,
     def_ids: DefIdCache<'tcx>,
+    pub owner_fn_id: DefId,
     typing_env: mir_ty::TypingEnv<'tcx>,
     /// Maps index in [`mir_ty::ParamTy`] to [`rty::TypeParamIdx`].
     /// These indices may differ because we skip lifetime parameters and they always need to be
     /// mapped when we translate a [`mir_ty::ParamTy`] to [`rty::ParamType`].
     /// See [`rty::TypeParamIdx`] for more details.
     param_idx_mapping: HashMap<u32, rty::TypeParamIdx>,
+    type_params: Rc<RefCell<TypeParamMap>>,
+    system: Rc<RefCell<chc::System>>,
 }
 
 impl<'tcx> TypeBuilder<'tcx> {
-    pub fn new(tcx: mir_ty::TyCtxt<'tcx>, def_ids: DefIdCache<'tcx>, def_id: DefId) -> Self {
-        let generics = tcx.generics_of(def_id);
+    pub fn new(
+        tcx: mir_ty::TyCtxt<'tcx>,
+        def_ids: DefIdCache<'tcx>,
+        owner_fn_id: DefId,
+        type_params: Rc<RefCell<TypeParamMap>>,
+        system: Rc<RefCell<chc::System>>,
+    ) -> Self {
+        let generics = tcx.generics_of(owner_fn_id);
         let mut param_idx_mapping: HashMap<u32, rty::TypeParamIdx> = Default::default();
         for i in 0..generics.count() {
             let generic_param = generics.param_at(i, tcx);
@@ -93,21 +104,40 @@ impl<'tcx> TypeBuilder<'tcx> {
                 mir_ty::GenericParamDefKind::Const { .. } => {}
             }
         }
-        let typing_env = mir_ty::TypingEnv::post_analysis(tcx, def_id);
+
+        tracing::debug!("TypeBuilder is created for {owner_fn_id:?}.");
+        let typing_env = mir_ty::TypingEnv::post_analysis(tcx, owner_fn_id);
         Self {
             tcx,
             def_ids,
+            owner_fn_id,
             typing_env,
             param_idx_mapping,
+            type_params,
+            system,
         }
     }
 
     fn translate_param_type(&self, ty: &mir_ty::ParamTy) -> rty::Type<rty::Closed> {
-        let index = *self
+        let param_local_idx = *self
             .param_idx_mapping
             .get(&ty.index)
             .expect("unknown type param idx");
-        rty::ParamType::new(index).into()
+
+        let mut type_params = self.type_params.borrow_mut();
+        let forall_sort_idx = type_params
+            .entry(TypeParam::GenericType(self.owner_fn_id, ty.index))
+            .or_insert_with(|| {
+                let idx = self.system.borrow_mut().new_forall_sort();
+                tracing::debug!(
+                    "issue the new ForallSortIdx {} for ParamTy {:?} at {:?}.",
+                    idx,
+                    ty,
+                    self.owner_fn_id
+                );
+                idx
+            });
+        rty::ParamType::new(param_local_idx, *forall_sort_idx).into()
     }
 
     /// Replaces {closure} types with thrust_models::Closure<{closure}>.
@@ -152,19 +182,32 @@ impl<'tcx> TypeBuilder<'tcx> {
     }
 
     fn resolve_model_ty(&self, orig_ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> {
+        tracing::debug!("attempting to resolve the type {:#?}.", orig_ty);
         let ty = self.replace_closure_model(orig_ty);
 
         let Some(model_ty_def_id) = self.def_ids.model_ty() else {
             return ty;
         };
         let args = self.tcx.mk_args(&[ty.into()]);
+        tracing::debug!("generic args are {:#?}.", args);
         let projection_ty = mir_ty::Ty::new_projection(self.tcx, model_ty_def_id, args);
         if let Ok(normalized_ty) = self
             .tcx
             .try_normalize_erasing_regions(self.typing_env, projection_ty)
         {
-            return normalized_ty;
+            tracing::debug!("the type {:#?} is resolved as the type {:#?}.", orig_ty, ty);
+            let contains_model_ty_alias = normalized_ty.walk().any(|arg| {
+                if let mir_ty::GenericArgKind::Type(t) = arg.kind() {
+                    matches!(t.kind(), mir_ty::TyKind::Alias(_, alias_ty) if alias_ty.def_id == model_ty_def_id)
+                } else {
+                    false
+                }
+            });
+            if !contains_model_ty_alias {
+                return normalized_ty;
+            }
         }
+        tracing::debug!("the type {:#?} is replaced as the {:#?}.", orig_ty, ty);
         ty
     }
 
@@ -258,6 +301,7 @@ impl<'tcx> TypeBuilder<'tcx> {
                     unimplemented!("unsupported ADT: {:?}", ty);
                 }
             }
+            // mir_ty::TyKind::Alias(_, ty) => self.translate_alias_type(ty),
             kind => unimplemented!("unrefined_ty: {:?}", kind),
         }
     }
diff --git a/src/rty.rs b/src/rty.rs
index 32456b45..9eb3381e 100644
--- a/src/rty.rs
+++ b/src/rty.rs
@@ -43,7 +43,7 @@ use pretty::{termcolor, Pretty};
 use rustc_abi::VariantIdx;
 use rustc_index::IndexVec;
 
-use crate::chc;
+use crate::chc::{self, ForallSortIdx};
 
 mod template;
 pub use template::{Template, TemplateBuilder};
@@ -609,7 +609,8 @@ impl<T> EnumType<T> {
 /// A type parameter.
 #[derive(Debug, Clone)]
 pub struct ParamType {
-    pub idx: TypeParamIdx,
+    type_param_idx: TypeParamIdx,
+    forall_sort_idx: ForallSortIdx,
 }
 
 impl<'a, D> Pretty<'a, D, termcolor::ColorSpec> for &ParamType
@@ -617,17 +618,24 @@ where
     D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
 {
     fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
-        self.idx.pretty(allocator)
+        self.type_param_idx.pretty(allocator)
     }
 }
 
 impl ParamType {
-    pub fn new(idx: TypeParamIdx) -> Self {
-        ParamType { idx }
+    pub fn new(type_param_idx: TypeParamIdx, forall_sort_idx: ForallSortIdx) -> Self {
+        ParamType {
+            type_param_idx,
+            forall_sort_idx,
+        }
+    }
+
+    pub fn type_param_index(&self) -> TypeParamIdx {
+        self.type_param_idx
     }
 
-    pub fn index(&self) -> TypeParamIdx {
-        self.idx
+    pub fn forall_sort_index(&self) -> ForallSortIdx {
+        self.forall_sort_idx
     }
 
     pub fn into_closed_ty(self) -> Type<Closed> {
@@ -914,7 +922,7 @@ impl<T> Type<T> {
             //       currently String sort seems not available in HORN logic of Z3
             Type::String => chc::Sort::null(),
             Type::Never => chc::Sort::null(),
-            Type::Param(ty) => chc::Sort::param(ty.index().into()),
+            Type::Param(ty) => chc::Sort::forall(ty.forall_sort_index()),
             Type::Pointer(ty) => {
                 let elem_sort = ty.elem.ty.to_sort();
 
@@ -1000,7 +1008,7 @@ impl<T> Type<T> {
     pub fn free_ty_params(&self) -> HashSet<TypeParamIdx> {
         match self {
             Type::Int | Type::Bool | Type::String | Type::Never => Default::default(),
-            Type::Param(ty) => std::iter::once(ty.index()).collect(),
+            Type::Param(ty) => std::iter::once(ty.type_param_index()).collect(),
             Type::Pointer(ty) => ty.free_ty_params(),
             Type::Function(ty) => ty.free_ty_params(),
             Type::Tuple(ty) => ty.free_ty_params(),
@@ -1567,7 +1575,7 @@ impl<FV> RefinedType<FV> {
         match &mut self.ty {
             Type::Int | Type::Bool | Type::String | Type::Never => {}
             Type::Param(ty) => {
-                if let Some(rty) = subst.get(ty.index()) {
+                if let Some(rty) = subst.get(ty.type_param_index()) {
                     let RefinedType {
                         ty: replacement_ty,
                         refinement,
@@ -1603,15 +1611,15 @@ impl<FV> RefinedType<FV> {
             | (Type::Bool, Type::Bool)
             | (Type::String, Type::String)
             | (Type::Never, Type::Never) => Default::default(),
-            (Type::Param(pty), ty) if !ty.free_ty_params().contains(&pty.index()) => {
+            (Type::Param(pty), ty) if !ty.free_ty_params().contains(&pty.type_param_index()) => {
                 TypeParamSubst::singleton(
-                    pty.index(),
+                    pty.type_param_index(),
                     RefinedType::new(ty.clone(), other.refinement.clone()),
                 )
             }
-            (ty, Type::Param(pty)) if !ty.free_ty_params().contains(&pty.index()) => {
+            (ty, Type::Param(pty)) if !ty.free_ty_params().contains(&pty.type_param_index()) => {
                 TypeParamSubst::singleton(
-                    pty.index(),
+                    pty.type_param_index(),
                     RefinedType::new(ty.clone(), self.refinement.clone()),
                 )
             }
@@ -1637,7 +1645,11 @@ impl RefinedType<Closed> {
 /// Substitutes type parameters in a sort.
 fn subst_ty_params_in_sort<T>(sort: &mut chc::Sort, subst: &TypeParamSubst<T>) {
     match sort {
-        chc::Sort::Null | chc::Sort::Int | chc::Sort::Bool | chc::Sort::String => {}
+        chc::Sort::Null
+        | chc::Sort::Int
+        | chc::Sort::Bool
+        | chc::Sort::String
+        | chc::Sort::Forall(_) => {}
         chc::Sort::Param(idx) => {
             let type_param_idx = TypeParamIdx::from_usize(*idx);
             if let Some(rty) = subst.get(type_param_idx) {
diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs
index 20d6f341..092116d5 100644
--- a/src/rty/subtyping.rs
+++ b/src/rty/subtyping.rs
@@ -120,6 +120,8 @@ where
                 let cs2 = self.relate_sub_refined_type(&got.elem, &expected.elem);
                 clauses.extend(cs2);
             }
+            (Type::Param(got), Type::Param(expected))
+                if got.forall_sort_idx == expected.forall_sort_idx => {}
             _ => panic!(
                 "inconsistent types: got={}, expected={}",
                 got.display(),
diff --git a/std.rs b/std.rs
index dc30924e..fdaa4cf8 100644
--- a/std.rs
+++ b/std.rs
@@ -304,378 +304,378 @@ mod thrust_models {
     }
 }
 
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == thrust_models::model::Box::new(x))]
-fn _extern_spec_box_new<T>(x: T) -> Box<T> where T: thrust_models::Model, T::Ty: PartialEq {
-    Box::new(x)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == (x == y))]
-fn _extern_spec_box_partialeq_eq<T>(x: &Box<T>, y: &Box<T>) -> bool
-  where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
-{
-    <Box<T> as PartialEq>::eq(x, y)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(*x == !y && *y == !x)]
-fn _extern_spec_std_mem_swap<T>(x: &mut T, y: &mut T) where T: thrust_models::Model, T::Ty: PartialEq {
-    std::mem::swap(x, y)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(!dest == src && result == *dest)]
-fn _extern_spec_std_mem_replace<T>(dest: &mut T, src: T) -> T where T: thrust_models::Model, T::Ty: PartialEq {
-    std::mem::replace(dest, src)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == (x == y))]
-fn _extern_spec_option_partialeq_eq<T>(x: &Option<T>, y: &Option<T>) -> bool
-  where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
-{
-    <Option<T> as PartialEq>::eq(x, y)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(opt != None)]
-#[thrust_macros::ensures(Some(result) == opt)]
-fn _extern_spec_option_unwrap<T>(opt: Option<T>) -> T where T: thrust_models::Model, T::Ty: PartialEq {
-    Option::unwrap(opt)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    (*opt == None && result == true)
-    || (*opt != None && result == false)
-)]
-fn _extern_spec_option_is_none<T>(opt: &Option<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
-    Option::is_none(opt)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    (*opt == None && result == false)
-    || (*opt != None && result == true)
-)]
-fn _extern_spec_option_is_some<T>(opt: &Option<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
-    Option::is_some(opt)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    (opt != None && Some(result) == opt)
-    || (opt == None && result == default)
-)]
-fn _extern_spec_option_unwrap_or<T>(opt: Option<T>, default: T) -> T where T: thrust_models::Model, T::Ty: PartialEq {
-    Option::unwrap_or(opt, default)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    (thrust_models::exists(|x| opt == Some(x) && result == Ok(x)))
-    || (opt == None && result == Err(err))
-)]
-fn _extern_spec_option_ok_or<T, E>(opt: Option<T>, err: E) -> Result<T, E>
-    where T: thrust_models::Model, T::Ty: PartialEq,
-          E: thrust_models::Model, E::Ty: PartialEq,
-{
-    Option::ok_or(opt, err)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(!opt == None && result == *opt)]
-fn _extern_spec_option_take<T>(opt: &mut Option<T>) -> Option<T> where T: thrust_models::Model, T::Ty: PartialEq {
-    Option::take(opt)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(!opt == Some(src) && result == *opt)]
-fn _extern_spec_option_replace<T>(opt: &mut Option<T>, src: T) -> Option<T>
-    where T: thrust_models::Model, T::Ty: PartialEq
-{
-    Option::replace(opt, src)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    thrust_models::exists(|x| opt == &Some(x) && result == Some(&x))
-    || (opt == &None && result == None)
-)]
-fn _extern_spec_option_as_ref<T>(opt: &Option<T>) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq {
-    Option::as_ref(opt)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    thrust_models::exists(|x1, x2|
-      *opt == Some(x1) &&
-      !opt == Some(x2) &&
-      result == Some(thrust_models::model::Mut::new(x1, x2))
-    )
-    || (
-      *opt == None &&
-      !opt == None &&
-      result == None
-    )
-)]
-fn _extern_spec_option_as_mut<T>(opt: &mut Option<T>) -> Option<&mut T>
-  where T: thrust_models::Model, T::Ty: PartialEq
-{
-    Option::as_mut(opt)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == (x == y))]
-fn _extern_spec_result_partialeq_eq<T, E>(x: &Result<T, E>, y: &Result<T, E>) -> bool
-  where T: thrust_models::Model + PartialEq, T::Ty: PartialEq,
-        E: thrust_models::Model + PartialEq, E::Ty: PartialEq,
-{
-    <Result<T, E> as PartialEq>::eq(x, y)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(thrust_models::exists(|x| res == Ok(x)))]
-#[thrust_macros::ensures(Ok(result) == res)]
-fn _extern_spec_result_unwrap<T, E: std::fmt::Debug>(res: Result<T, E>) -> T
-  where T: thrust_models::Model, T::Ty: PartialEq,
-        E: thrust_models::Model, E::Ty: PartialEq,
-{
-    Result::unwrap(res)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(thrust_models::exists(|x| res == Err(x)))]
-#[thrust_macros::ensures(Err(result) == res)]
-fn _extern_spec_result_unwrap_err<T: std::fmt::Debug, E>(res: Result<T, E>) -> E
-  where T: thrust_models::Model, T::Ty: PartialEq,
-        E: thrust_models::Model, E::Ty: PartialEq,
-{
-    Result::unwrap_err(res)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    thrust_models::exists(|x| res == Ok(x) && result == Some(x))
-    || thrust_models::exists(|x| res == Err(x) && result == None)
-)]
-fn _extern_spec_result_ok<T, E>(res: Result<T, E>) -> Option<T>
-  where T: thrust_models::Model, T::Ty: PartialEq,
-        E: thrust_models::Model, E::Ty: PartialEq,
-{
-    Result::ok(res)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    thrust_models::exists(|x| res == Ok(x) && result == None)
-    || thrust_models::exists(|x| res == Err(x) && result == Some(x))
-)]
-fn _extern_spec_result_err<T, E>(res: Result<T, E>) -> Option<E>
-  where T: thrust_models::Model, T::Ty: PartialEq,
-        E: thrust_models::Model, E::Ty: PartialEq,
-{
-    Result::err(res)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    thrust_models::exists(|x| *res == Ok(x) && result == true)
-    || thrust_models::exists(|x| *res == Err(x) && result == false)
-)]
-fn _extern_spec_result_is_ok<T, E>(res: &Result<T, E>) -> bool
-  where T: thrust_models::Model, T::Ty: PartialEq,
-        E: thrust_models::Model, E::Ty: PartialEq,
-{
-    Result::is_ok(res)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    thrust_models::exists(|x| *res == Ok(x) && result == false)
-    || thrust_models::exists(|x| *res == Err(x) && result == true)
-)]
-fn _extern_spec_result_is_err<T, E>(res: &Result<T, E>) -> bool
-  where T: thrust_models::Model, T::Ty: PartialEq,
-        E: thrust_models::Model, E::Ty: PartialEq,
-{
-    Result::is_err(res)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)] // TODO: require x != i32::MIN
-#[thrust_macros::ensures(result >= 0 && (result == x || result == -x))]
-fn _extern_spec_i32_abs(x: i32) -> i32 {
-    i32::abs(x)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    (x >= y && result == (x - y))
-    || (x < y && result == (y - x))
-)]
-fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 {
-    i32::abs_diff(x, y)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))]
-fn _extern_spec_i32_signum(x: i32) -> i32 {
-    i32::signum(x)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures((x < 0 && result == false) || (x >= 0 && result == true))]
-fn _extern_spec_i32_is_positive(x: i32) -> bool {
-    i32::is_positive(x)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures((x <= 0 && result == true) || (x > 0 && result == false))]
-fn _extern_spec_i32_is_negative(x: i32) -> bool {
-    i32::is_negative(x)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result.1 == 0)]
-fn _extern_spec_vec_new<T>() -> Vec<T> where T: thrust_models::Model, T::Ty: PartialEq {
-    Vec::<T>::new()
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(!vec == thrust_models::model::Vec((*vec).0.store((*vec).1, elem), (*vec).1 + 1))]
-fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T)
-    where T: thrust_models::Model, T::Ty: PartialEq
-{
-    Vec::push(vec, elem)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == vec.1)]
-fn _extern_spec_vec_len<T>(vec: &Vec<T>) -> usize where T: thrust_models::Model, T::Ty: PartialEq {
-    Vec::len(vec)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(index < vec.1)]
-#[thrust_macros::ensures(*result == vec.0[index])]
-fn _extern_spec_vec_index<T>(vec: &Vec<T>, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq {
-    <Vec<T> as std::ops::Index<usize>>::index(vec, index)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(index < (*vec).1)]
-#[thrust_macros::ensures(
-    *result == (*vec).0[index] &&
-    !result == (!vec).0[index] &&
-    !vec == thrust_models::model::Vec((*vec).0.store(index, !result), (*vec).1)
-)]
-fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T
-    where T: thrust_models::Model, T::Ty: PartialEq
-{
-    <Vec<T> as std::ops::IndexMut<usize>>::index_mut(vec, index)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures((!vec).1 == 0)]
-fn _extern_spec_vec_clear<T>(vec: &mut Vec<T>) where T: thrust_models::Model, T::Ty: PartialEq {
-    Vec::clear(vec)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    (!vec).0 == (*vec).0 && (
-        (
-            (*vec).1 > 0 &&
-            (!vec).1 == (*vec).1 - 1 &&
-            result == Some((*vec).0[(*vec).1 - 1])
-        ) || (
-            (*vec).1 == 0 &&
-            (!vec).1 == 0 &&
-            result == None
-        )
-    )
-)]
-fn _extern_spec_vec_pop<T>(vec: &mut Vec<T>) -> Option<T> where T: thrust_models::Model, T::Ty: PartialEq {
-    Vec::pop(vec)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == ((*vec).1 == 0))]
-fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
-    Vec::is_empty(vec)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(
-    (
-        (*vec).1 > len &&
-        !vec == thrust_models::model::Vec((*vec).0, len)
-    ) || (
-        (*vec).1 <= len &&
-        !vec == *vec
-    )
-)]
-fn _extern_spec_vec_truncate<T>(vec: &mut Vec<T>, len: usize) where T: thrust_models::Model, T::Ty: PartialEq {
-    Vec::truncate(vec, len)
-}
-
-// TODO: The following specs of some trait methods are too restrictive; we should allow for a
-//       per-impl spec once we can describe the spec of blanket impls.
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == (*x == *y))]
-fn _extern_spec_partialeq_eq<T>(x: &T, y: &T) -> bool
-  where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
-{
-    PartialEq::eq(x, y)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == (*x < *y))]
-fn _extern_spec_partialord_lt<T>(x: &T, y: &T) -> bool
-  where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd
-{
-    PartialOrd::lt(x, y)
-}
-
-#[thrust::extern_spec_fn]
-#[thrust_macros::requires(true)]
-#[thrust_macros::ensures(result == (*x > *y))]
-fn _extern_spec_partialord_gt<T>(x: &T, y: &T) -> bool
-  where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd
-{
-    PartialOrd::gt(x, y)
-}
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result == thrust_models::model::Box::new(x))]
+// fn _extern_spec_box_new<T>(x: T) -> Box<T> where T: thrust_models::Model, T::Ty: PartialEq {
+//     Box::new(x)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result == (x == y))]
+// fn _extern_spec_box_partialeq_eq<T>(x: &Box<T>, y: &Box<T>) -> bool
+//   where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
+// {
+//     <Box<T> as PartialEq>::eq(x, y)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(*x == !y && *y == !x)]
+// fn _extern_spec_std_mem_swap<T>(x: &mut T, y: &mut T) where T: thrust_models::Model, T::Ty: PartialEq {
+//     std::mem::swap(x, y)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(!dest == src && result == *dest)]
+// fn _extern_spec_std_mem_replace<T>(dest: &mut T, src: T) -> T where T: thrust_models::Model, T::Ty: PartialEq {
+//     std::mem::replace(dest, src)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result == (x == y))]
+// fn _extern_spec_option_partialeq_eq<T>(x: &Option<T>, y: &Option<T>) -> bool
+//   where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
+// {
+//     <Option<T> as PartialEq>::eq(x, y)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(opt != None)]
+// #[thrust_macros::ensures(Some(result) == opt)]
+// fn _extern_spec_option_unwrap<T>(opt: Option<T>) -> T where T: thrust_models::Model, T::Ty: PartialEq {
+//     Option::unwrap(opt)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     (*opt == None && result == true)
+//     || (*opt != None && result == false)
+// )]
+// fn _extern_spec_option_is_none<T>(opt: &Option<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
+//     Option::is_none(opt)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     (*opt == None && result == false)
+//     || (*opt != None && result == true)
+// )]
+// fn _extern_spec_option_is_some<T>(opt: &Option<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
+//     Option::is_some(opt)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     (opt != None && Some(result) == opt)
+//     || (opt == None && result == default)
+// )]
+// fn _extern_spec_option_unwrap_or<T>(opt: Option<T>, default: T) -> T where T: thrust_models::Model, T::Ty: PartialEq {
+//     Option::unwrap_or(opt, default)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     (thrust_models::exists(|x| opt == Some(x) && result == Ok(x)))
+//     || (opt == None && result == Err(err))
+// )]
+// fn _extern_spec_option_ok_or<T, E>(opt: Option<T>, err: E) -> Result<T, E>
+//     where T: thrust_models::Model, T::Ty: PartialEq,
+//           E: thrust_models::Model, E::Ty: PartialEq,
+// {
+//     Option::ok_or(opt, err)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(!opt == None && result == *opt)]
+// fn _extern_spec_option_take<T>(opt: &mut Option<T>) -> Option<T> where T: thrust_models::Model, T::Ty: PartialEq {
+//     Option::take(opt)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(!opt == Some(src) && result == *opt)]
+// fn _extern_spec_option_replace<T>(opt: &mut Option<T>, src: T) -> Option<T>
+//     where T: thrust_models::Model, T::Ty: PartialEq
+// {
+//     Option::replace(opt, src)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     thrust_models::exists(|x| opt == &Some(x) && result == Some(&x))
+//     || (opt == &None && result == None)
+// )]
+// fn _extern_spec_option_as_ref<T>(opt: &Option<T>) -> Option<&T> where T: thrust_models::Model, T::Ty: PartialEq {
+//     Option::as_ref(opt)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     thrust_models::exists(|x1, x2|
+//       *opt == Some(x1) &&
+//       !opt == Some(x2) &&
+//       result == Some(thrust_models::model::Mut::new(x1, x2))
+//     )
+//     || (
+//       *opt == None &&
+//       !opt == None &&
+//       result == None
+//     )
+// )]
+// fn _extern_spec_option_as_mut<T>(opt: &mut Option<T>) -> Option<&mut T>
+//   where T: thrust_models::Model, T::Ty: PartialEq
+// {
+//     Option::as_mut(opt)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result == (x == y))]
+// fn _extern_spec_result_partialeq_eq<T, E>(x: &Result<T, E>, y: &Result<T, E>) -> bool
+//   where T: thrust_models::Model + PartialEq, T::Ty: PartialEq,
+//         E: thrust_models::Model + PartialEq, E::Ty: PartialEq,
+// {
+//     <Result<T, E> as PartialEq>::eq(x, y)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(thrust_models::exists(|x| res == Ok(x)))]
+// #[thrust_macros::ensures(Ok(result) == res)]
+// fn _extern_spec_result_unwrap<T, E: std::fmt::Debug>(res: Result<T, E>) -> T
+//   where T: thrust_models::Model, T::Ty: PartialEq,
+//         E: thrust_models::Model, E::Ty: PartialEq,
+// {
+//     Result::unwrap(res)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(thrust_models::exists(|x| res == Err(x)))]
+// #[thrust_macros::ensures(Err(result) == res)]
+// fn _extern_spec_result_unwrap_err<T: std::fmt::Debug, E>(res: Result<T, E>) -> E
+//   where T: thrust_models::Model, T::Ty: PartialEq,
+//         E: thrust_models::Model, E::Ty: PartialEq,
+// {
+//     Result::unwrap_err(res)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     thrust_models::exists(|x| res == Ok(x) && result == Some(x))
+//     || thrust_models::exists(|x| res == Err(x) && result == None)
+// )]
+// fn _extern_spec_result_ok<T, E>(res: Result<T, E>) -> Option<T>
+//   where T: thrust_models::Model, T::Ty: PartialEq,
+//         E: thrust_models::Model, E::Ty: PartialEq,
+// {
+//     Result::ok(res)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     thrust_models::exists(|x| res == Ok(x) && result == None)
+//     || thrust_models::exists(|x| res == Err(x) && result == Some(x))
+// )]
+// fn _extern_spec_result_err<T, E>(res: Result<T, E>) -> Option<E>
+//   where T: thrust_models::Model, T::Ty: PartialEq,
+//         E: thrust_models::Model, E::Ty: PartialEq,
+// {
+//     Result::err(res)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     thrust_models::exists(|x| *res == Ok(x) && result == true)
+//     || thrust_models::exists(|x| *res == Err(x) && result == false)
+// )]
+// fn _extern_spec_result_is_ok<T, E>(res: &Result<T, E>) -> bool
+//   where T: thrust_models::Model, T::Ty: PartialEq,
+//         E: thrust_models::Model, E::Ty: PartialEq,
+// {
+//     Result::is_ok(res)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     thrust_models::exists(|x| *res == Ok(x) && result == false)
+//     || thrust_models::exists(|x| *res == Err(x) && result == true)
+// )]
+// fn _extern_spec_result_is_err<T, E>(res: &Result<T, E>) -> bool
+//   where T: thrust_models::Model, T::Ty: PartialEq,
+//         E: thrust_models::Model, E::Ty: PartialEq,
+// {
+//     Result::is_err(res)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)] // TODO: require x != i32::MIN
+// #[thrust_macros::ensures(result >= 0 && (result == x || result == -x))]
+// fn _extern_spec_i32_abs(x: i32) -> i32 {
+//     i32::abs(x)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     (x >= y && result == (x - y))
+//     || (x < y && result == (y - x))
+// )]
+// fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 {
+//     i32::abs_diff(x, y)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))]
+// fn _extern_spec_i32_signum(x: i32) -> i32 {
+//     i32::signum(x)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures((x < 0 && result == false) || (x >= 0 && result == true))]
+// fn _extern_spec_i32_is_positive(x: i32) -> bool {
+//     i32::is_positive(x)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures((x <= 0 && result == true) || (x > 0 && result == false))]
+// fn _extern_spec_i32_is_negative(x: i32) -> bool {
+//     i32::is_negative(x)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result.1 == 0)]
+// fn _extern_spec_vec_new<T>() -> Vec<T> where T: thrust_models::Model, T::Ty: PartialEq {
+//     Vec::<T>::new()
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(!vec == thrust_models::model::Vec((*vec).0.store((*vec).1, elem), (*vec).1 + 1))]
+// fn _extern_spec_vec_push<T>(vec: &mut Vec<T>, elem: T)
+//     where T: thrust_models::Model, T::Ty: PartialEq
+// {
+//     Vec::push(vec, elem)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result == vec.1)]
+// fn _extern_spec_vec_len<T>(vec: &Vec<T>) -> usize where T: thrust_models::Model, T::Ty: PartialEq {
+//     Vec::len(vec)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(index < vec.1)]
+// #[thrust_macros::ensures(*result == vec.0[index])]
+// fn _extern_spec_vec_index<T>(vec: &Vec<T>, index: usize) -> &T where T: thrust_models::Model, T::Ty: PartialEq {
+//     <Vec<T> as std::ops::Index<usize>>::index(vec, index)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(index < (*vec).1)]
+// #[thrust_macros::ensures(
+//     *result == (*vec).0[index] &&
+//     !result == (!vec).0[index] &&
+//     !vec == thrust_models::model::Vec((*vec).0.store(index, !result), (*vec).1)
+// )]
+// fn _extern_spec_vec_index_mut<T>(vec: &mut Vec<T>, index: usize) -> &mut T
+//     where T: thrust_models::Model, T::Ty: PartialEq
+// {
+//     <Vec<T> as std::ops::IndexMut<usize>>::index_mut(vec, index)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures((!vec).1 == 0)]
+// fn _extern_spec_vec_clear<T>(vec: &mut Vec<T>) where T: thrust_models::Model, T::Ty: PartialEq {
+//     Vec::clear(vec)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     (!vec).0 == (*vec).0 && (
+//         (
+//             (*vec).1 > 0 &&
+//             (!vec).1 == (*vec).1 - 1 &&
+//             result == Some((*vec).0[(*vec).1 - 1])
+//         ) || (
+//             (*vec).1 == 0 &&
+//             (!vec).1 == 0 &&
+//             result == None
+//         )
+//     )
+// )]
+// fn _extern_spec_vec_pop<T>(vec: &mut Vec<T>) -> Option<T> where T: thrust_models::Model, T::Ty: PartialEq {
+//     Vec::pop(vec)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result == ((*vec).1 == 0))]
+// fn _extern_spec_vec_is_empty<T>(vec: &Vec<T>) -> bool where T: thrust_models::Model, T::Ty: PartialEq {
+//     Vec::is_empty(vec)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(
+//     (
+//         (*vec).1 > len &&
+//         !vec == thrust_models::model::Vec((*vec).0, len)
+//     ) || (
+//         (*vec).1 <= len &&
+//         !vec == *vec
+//     )
+// )]
+// fn _extern_spec_vec_truncate<T>(vec: &mut Vec<T>, len: usize) where T: thrust_models::Model, T::Ty: PartialEq {
+//     Vec::truncate(vec, len)
+// }
+
+// // TODO: The following specs of some trait methods are too restrictive; we should allow for a
+// //       per-impl spec once we can describe the spec of blanket impls.
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result == (*x == *y))]
+// fn _extern_spec_partialeq_eq<T>(x: &T, y: &T) -> bool
+//   where T: thrust_models::Model + PartialEq, T::Ty: PartialEq
+// {
+//     PartialEq::eq(x, y)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result == (*x < *y))]
+// fn _extern_spec_partialord_lt<T>(x: &T, y: &T) -> bool
+//   where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd
+// {
+//     PartialOrd::lt(x, y)
+// }
+
+// #[thrust::extern_spec_fn]
+// #[thrust_macros::requires(true)]
+// #[thrust_macros::ensures(result == (*x > *y))]
+// fn _extern_spec_partialord_gt<T>(x: &T, y: &T) -> bool
+//   where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd
+// {
+//     PartialOrd::gt(x, y)
+// }
diff --git a/tests/ui/pass/traits/simple_loop.rs b/tests/ui/pass/traits/simple_loop.rs
new file mode 100644
index 00000000..857ecdb3
--- /dev/null
+++ b/tests/ui/pass/traits/simple_loop.rs
@@ -0,0 +1,28 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper THRUST_SOLVER_TIMEOUT_SECS=60
+
+#[thrust_macros::context]
+trait A {
+    #[thrust_macros::requires(Self::p(x))]
+    #[thrust_macros::ensures(Self::p(result))]
+    fn f(&self, x: i64) -> i64;
+
+    #[thrust_macros::predicate]
+    fn p(x: i64) -> bool;
+}
+
+#[thrust_macros::requires(T::p(x))]
+#[thrust_macros::ensures(T::p(result))]
+fn target<T: A>(a: &T, x: i64) -> i64 {
+    let mut v = x;
+    let mut i = 0;
+    while i < 3 {
+        v = a.f(v);
+        i += 1;
+    }
+
+    v
+}
+
+fn main() {}