diff --git a/src/analysis/typepal/Collector.rsc b/src/analysis/typepal/Collector.rsc
index a5fae44..8971164 100644
--- a/src/analysis/typepal/Collector.rsc
+++ b/src/analysis/typepal/Collector.rsc
@@ -215,6 +215,8 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co
     Defines defines = {};
     Defines addedDefines = {};
 
+    map[loc,loc] define2id = ();
+
     map[loc,loc] logical2physical = ();
 
     map[loc,loc] physical2logical = ();
@@ -261,12 +263,21 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co
 
     bool building = true;
 
-    void collector_define(str orgId, IdRole idRole, value def, DefInfo info){
+    void collector_define(value id, IdRole idRole, value def, DefInfo info){
         if(building){
             loc l = |undefined:///|;
             if(Tree tdef := def) l = getLoc(tdef);
             else if(loc ldef := def) l = ldef;
             else throw TypePalUsage("Argument `def` of `define` should be `Tree` or `loc`, found <typeOf(def)>");
+
+            str orgId = "";
+            if(Tree tid := id) {
+                orgId = "<tid>";
+                define2id[l] = tid.src;
+            }
+            else if(str sid := id) orgId = sid;
+            else throw TypePalUsage("Argument `id` of `define` should be `Tree` or `str`, found <typeOf(orgId)>");
+
             nname = normalizeName(orgId);
             Define newDef = <currentScope, nname, orgId, idRole, l, info>;
             logL = buildLogical2physical(newDef);
@@ -334,7 +345,7 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co
         return false;
     }
 
-    void collector_defineInScope(value scope, str orgId, IdRole idRole, value def, DefInfo info){
+    void collector_defineInScope(value scope, value id, IdRole idRole, value def, DefInfo info){
         if(building){
             loc definingScope = |undefined:///|;
             if(Tree tscope := scope) definingScope = getLoc(tscope);
@@ -346,6 +357,14 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co
             else if(loc ldef := def) l = ldef;
             else throw TypePalUsage("Argument `def` of `defineInScope` should be `Tree` or `loc`, found <typeOf(def)>");
 
+            str orgId = "";
+            if(Tree tid := id) {
+                orgId = "<tid>";
+                define2id[l] = tid.src;
+            }
+            else if(str sid := id) orgId = sid;
+            else throw TypePalUsage("Argument `id` of `defineInScope` should be `Tree` or `str`, found <typeOf(orgId)>");
+
             nname = normalizeName(orgId);
             Define newDef = <definingScope, nname, orgId, idRole, l, info>;
             logL = buildLogical2physical(newDef);
@@ -1022,7 +1041,8 @@ Collector newCollector(str modelName, map[str,Tree] namedTrees, TypePalConfig co
            }
            tm.definesMap = definesMap;
            definesMap = (); defines = addedDefines = {};
-
+           tm.define2id = define2id; define2id = ();
+           
            tm.scopes = toLogicalLocs(scopes - addedScopes) + addedScopes; scopes = addedScopes = ();
            tm.paths = toLogicalLocs(paths - addedPaths) + addedPaths; paths = addedPaths = {};
            tm.referPaths = toLogicalLocs(referPaths); referPaths = {};
diff --git a/src/analysis/typepal/ICollector.rsc b/src/analysis/typepal/ICollector.rsc
index d5df681..dd04261 100644
--- a/src/analysis/typepal/ICollector.rsc
+++ b/src/analysis/typepal/ICollector.rsc
@@ -47,8 +47,8 @@ data Collector
      /* Reporting */     bool (FailMessage msg) report,
                          bool (list[FailMessage] msgs) reports,
 
-     /* Define */        void (str id, IdRole idRole, value def, DefInfo info) define,
-                         void (value scope, str id, IdRole idRole, value def, DefInfo info) defineInScope,
+     /* Define */        void (value id, IdRole idRole, value def, DefInfo info) define,
+                         void (value scope, value id, IdRole idRole, value def, DefInfo info) defineInScope,
                          Tree (str id, IdRole idRole, value def, DefInfo info) predefine,
                          Tree (value scope, str id, IdRole idRole, DefInfo info) predefineInScope,
                          bool (str id, Tree useOrDef) isAlreadyDefined,
diff --git a/src/analysis/typepal/Solver.rsc b/src/analysis/typepal/Solver.rsc
index 8a4abab..2a118e9 100644
--- a/src/analysis/typepal/Solver.rsc
+++ b/src/analysis/typepal/Solver.rsc
@@ -62,6 +62,10 @@ void assertValidUseDef(TModel tm, Solver solver) {
     useLocs = sort([u.occ | u <- tm.uses], isLexicallyLess);
     defLocs = sort([d.defined | d <- tm.defines], isLexicallyLess);
     for (pair: <useLoc, defLoc> <- tm.useDef) {
+        // Invert `define2id` when needed
+        if (/Define d := tm.defines, defLoc == (tm.define2id[d.defined] ? |unknown:///|)) {
+            defLoc = d.defined;
+        }
 
         assert useLoc in useLocs :
             "Expected: For each `\<useLoc, defLoc\>` in `tm.useDef`, a corresponding `Use` exists in `tm.uses` for `useLoc`. " +
@@ -956,7 +960,10 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){
     Define solver_getDefine(loc l) = definitions[getLogicalLoc(l)];
 
     rel[loc,loc] solver_getUseDef()
-        = { *{<u, d> | loc d <- definedBy[u]} | loc u <- definedBy };
+        = { *{<u, resolveDef(d)> | loc d <- definedBy[u]} | loc u <- definedBy };
+
+    loc resolveDef(loc def)
+        =  tm.define2id[tm.logical2physical[def] ? def] ? def;
 
     bool solver_isContainedIn(loc inner, loc outer)
         = isContainedIn(inner, outer, logical2physical);
@@ -1790,7 +1797,7 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){
         tm.specializedFacts = specializedFacts;
 
         //println("definedBy;"); iprintln(definedBy);
-        tm.useDef = { *{<u, d> | loc d <- definedBy[u]} | loc u <- definedBy };
+        tm.useDef = solver_getUseDef();
 
         // Update `uses` with all uses resolved by the solver
         tm.uses = [*({*tm.uses} + {*def2uses[d] | d <- def2uses})];
diff --git a/src/analysis/typepal/TModel.rsc b/src/analysis/typepal/TModel.rsc
index d13feeb..c95bb85 100644
--- a/src/analysis/typepal/TModel.rsc
+++ b/src/analysis/typepal/TModel.rsc
@@ -115,6 +115,7 @@ data TModel (
     map[loc, Define] definitions = (),
     map[loc,loc] logical2physical = (),
     bool usesPhysicalLocs = false, // Are locations in physical format?
+    map[loc,loc] define2id = (),
     TypePalConfig config = tconfig()
 )   = tmodel();
 
diff --git a/src/examples/fwjava/Checker.rsc b/src/examples/fwjava/Checker.rsc
index a2c2123..0b4f718 100644
--- a/src/examples/fwjava/Checker.rsc
+++ b/src/examples/fwjava/Checker.rsc
@@ -102,7 +102,7 @@ TypePalConfig fwjConfig() =
 // ----  Collect --------------------------------------------------------------
 
 void collect(current: (ClassDecl) `class <ClassId cid> extends <ClassId ecid> { <FieldDecl* fieldDecls> <ConstructorDecl constructorDecl> <MethodDecl* methodDecls> }`, Collector c) {
-    c.define("<cid>", classId(), current, defType(classType("<cid>")));
+    c.define(cid, classId(), current, defType(classType("<cid>")));
     c.enterScope(current);
         c.push(key_extendsRelation, <"<cid>", "<ecid>">);
         scope = c.getScope();
@@ -131,22 +131,22 @@ void collect(current: (ConstructorDecl ) `<ClassId cid> <Formals formals> { <Sup
         c.report(error(current, "Expected constructor name %q, found %q", "<cid1>", "<cid>"));
     c.enterScope(current);
         tp = methodType(classType("<cid1>"), atypeList([classType("<f.cid>") | Formal f <- formals.formals]));
-        c.defineInScope(scope, "<cid>", constructorId(), current, defType(tp));
+        c.defineInScope(scope, cid, constructorId(), current, defType(tp));
         collect(formals, superCall, fieldAssignments, c);
     c.leaveScope(current);            
 }
 
 void collect(current: (Formal) `<ClassId cid> <Id id>`, Collector c){
-     c.define("<id>", formalId(), current, defType(classType("<cid>")));   
+     c.define(id, formalId(), current, defType(classType("<cid>")));   
 }
 
 void collect(fd: (FieldDecl) `<ClassId cid> <Id id> ;`, Collector c){
-     c.define("<id>", fieldId(), id, defType(classType("<cid>")));
+     c.define(id, fieldId(), id, defType(classType("<cid>")));
 }
 
 void collect(current: (MethodDecl) `<ClassId cid> <Id mid> <Formals formals> { return <Expression exp> ; }`,  Collector c){   
      formal_list =  [formal | formal <- formals.formals];
-     c.define("<mid>", methodId(), current, defType(formal_list + exp, AType(Solver s) { return methodType(s.getType(exp), atypeList([s.getType(formal) | formal <- formal_list])); }));
+     c.define(mid, methodId(), current, defType(formal_list + exp, AType(Solver s) { return methodType(s.getType(exp), atypeList([s.getType(formal) | formal <- formal_list])); }));
      c.enterScope(current);
          c.requireSubType(exp, classType("<cid>"), error(current,  "Actual return type %t should be subtype of declared return type %t", exp, cid));
          collect(formals, exp, c);
diff --git a/src/examples/fwjava/Test.rsc b/src/examples/fwjava/Test.rsc
index e62bfe4..44423cd 100644
--- a/src/examples/fwjava/Test.rsc
+++ b/src/examples/fwjava/Test.rsc
@@ -45,9 +45,18 @@ test bool fwjTModelTestCpt() = [] := fwjTModelFromName("cpt", false).messages;
 test bool fwjTModelTestPair() = [] := fwjTModelFromName("pair", false).messages;
 test bool fwjTModelTestTmp() = [_, _] := fwjTModelFromName("tmp", false).messages; // Two errors expected
 
-test bool fwjUseDefTestCpt() {
-    tm = fwjTModelFromName("cpt", false);
-    iprintln(tm.useDef);
+test bool fwjUseDefTestCpt() = fwjUseDefTest("cpt");
+test bool fwjUseDefTestPair() = fwjUseDefTest("pair");
+test bool fwjUseDefTestTmp() = fwjUseDefTest("tmp");
+
+private bool fwjUseDefTest(str name) {
+    tm = fwjTModelFromName(name, false);
+    for (<u, d> <- tm.useDef, u.length?, d.length?) {
+        // The following assertion is an indirect, but automatic/simple,
+        // approximation to check if `d` is the location of the identifier of a
+        // definition (instead of the whole definition).
+        assert u.length == d.length;
+    }
     return true;
 }