diff --git a/src/analysis/typepal/ConfigurableScopeGraph.rsc b/src/analysis/typepal/ConfigurableScopeGraph.rsc
index 5e61dc84..d6df65c9 100644
--- a/src/analysis/typepal/ConfigurableScopeGraph.rsc
+++ b/src/analysis/typepal/ConfigurableScopeGraph.rsc
@@ -108,6 +108,9 @@ data TypePalConfig(
         );
 
 data TypePalConfig(
+        bool assertValidDefines = false,
+        bool assertValidUseDef  = false,
+
         bool verbose               = false,
 
         PathConfig typepalPathConfig = pathConfig(),
diff --git a/src/analysis/typepal/Solver.rsc b/src/analysis/typepal/Solver.rsc
index dd5a46b3..8a4abab2 100644
--- a/src/analysis/typepal/Solver.rsc
+++ b/src/analysis/typepal/Solver.rsc
@@ -40,6 +40,63 @@ void checkAllTypesAvailable(TModel tm){
     }
 }
 
+void assertValidDefines(TModel tm){
+    if (!tm.config.assertValidDefines) return;
+    for(d <- tm.defines){
+
+        assert isContainedIn(d.defined, d.scope, tm.logical2physical) || "global-scope" == d.scope.scheme : 
+            "Expected: For each `d` in `tm.defines`, `d.defined` is contained in `d.scope`. " +
+            "Actual: For `<d>` in TModel `<tm.modelName>`, `<d.defined>` (`d.defined`) isn\'t contained in `<d.scope>` (`d.scope`).";
+
+        assert d.defInfo has atype : 
+            "Expected: For each `d` in `tm.defines`, field `d.defInfo` has field `atype`. " +
+            "Actual: For `<d>` in TModel `<tm.modelName>`, `<d.defInfo>` (`d.defInfo`) doesn\'t have that field.";
+    }
+}
+
+void assertValidUseDef(TModel tm, Solver solver) {
+    if (!tm.config.assertValidUseDef) return;
+    scopeGraph = newScopeGraph(tm, tm.config);
+    scopeGraph.setSolver(solver);
+
+    useLocs = sort([u.occ | u <- tm.uses], isLexicallyLess);
+    defLocs = sort([d.defined | d <- tm.defines], isLexicallyLess);
+    for (pair: <useLoc, defLoc> <- tm.useDef) {
+
+        assert useLoc in useLocs :
+            "Expected: For each `\<useLoc, defLoc\>` in `tm.useDef`, a corresponding `Use` exists in `tm.uses` for `useLoc`. " +
+            "Actual: For `<pair>` in TModel `<tm.modelName>`, a corresponding `Use` value doesn\'t exist for `<useLoc>` (`useLoc`), but it does for `<useLocs>`.";
+
+        assert defLoc in defLocs :
+            "Expected: For each `\<useLoc, defLoc\>` in `tm.useDef`, a corresponding `Define` exists in `tm.defines` for `defLoc`. " +
+            "Actual: For `<pair>` in TModel `<tm.modelName>`, a corresponding `Define` value doesn\'t exist for `<defLoc>` (`defLoc`), but it does for `<defLocs>`.";
+
+        usesAtUseLoc = [u | u <- tm.uses, useLoc == u.occ];
+        defsAtDefLoc = [d | d <- tm.defines, defLoc == d.defined];
+        reachable = (u: scopeGraph.lookup(u) | u <- usesAtUseLoc);
+        if (u <- usesAtUseLoc, d <- defsAtDefLoc, d.defined in reachable[u]) {
+
+            assert u.id == d.id :
+                "Expected: For each pair in `tm.useDef`, the corresponding `Use` `u` and `Define` `d` have equal `id` fields. " +
+                "Actual: For `<pair>` in TModel `<tm.modelName>`, `<u.id>` (`u.id`) isn\'t equal to `<d.id>` (`d.id`).";
+
+            assert u.orgId == d.orgId :
+                "Expected: For each pair in `tm.useDef`, the corresponding `Use` `u` and `Define` `d` have equal `orgId` fields. " +
+                "Actual: For `<pair>` in TModel `<tm.modelName>`, `<u.orgId>` (`u.orgId`) isn\'t equal to `<d.orgId>` (`d.orgId`).";
+
+            assert d.idRole in u.idRoles :
+                "Expected: For each pair in `tm.useDef`, the corresponding `Use` `u` and `Define` `d` have compatible roles. " +
+                "Actual: For `<pair>` in TModel `<tm.modelName>`, `<u.idRoles>` (`u.idRoles`) doesn\'t contain `<d.idRole>` (`d.idRole`).";
+
+        } else {
+
+            assert false : 
+                "Expected: For each `\<useLoc, defLoc\>` in `tm.useDef`, `defLoc` is reachable from `useLoc` in the scope graph. " +
+                "Actual: For `<pair>` in TModel `<tm.modelName>`, `<defLoc>` (`defLoc`) isn\'t reachable from `<useLoc>` (`useLoc`), but `<reachable>` are.";
+        }
+    }
+}
+
 // Implementation of the Solver data type: a collection of call backs
 
 Solver newSolver(Tree pt, TModel tm){
@@ -1735,6 +1792,9 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){
         //println("definedBy;"); iprintln(definedBy);
         tm.useDef = { *{<u, d> | loc d <- definedBy[u]} | loc u <- definedBy };
 
+        // Update `uses` with all uses resolved by the solver
+        tm.uses = [*({*tm.uses} + {*def2uses[d] | d <- def2uses})];
+
         ldefines = for(tup: <loc _, str _, str _, IdRole _, loc defined, DefInfo defInfo> <- tm.defines){
                         if(defInfo has tree){
                             l = getLogicalLoc(defInfo.tree);
@@ -1765,7 +1825,8 @@ Solver newSolver(map[str,Tree] namedTrees, TModel tm){
         messages =  visit(messages) { case loc l => solver_toPhysicalLoc(l) };
         tm.messages = sortMostPrecise(toList(toSet(messages)));
 
-        checkAllTypesAvailable(tm);
+        assertValidDefines(tm);
+        assertValidUseDef(tm, thisSolver);
         return tm;
     }
 
diff --git a/src/analysis/typepal/TestFramework.rsc b/src/analysis/typepal/TestFramework.rsc
index 64941574..dba94470 100644
--- a/src/analysis/typepal/TestFramework.rsc
+++ b/src/analysis/typepal/TestFramework.rsc
@@ -73,7 +73,7 @@ bool matches(str subject, str pat){
 str spinChar(int n)
     = n < 0 ? "|" : (0: "|", 1: "/", 2: "-", 3: "\\")[n%4];
 
-bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t) getModel, bool verbose = false, set[str] runOnly = {}, str runName = ""){
+bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t, str name) getModel, bool verbose = false, set[str] runOnly = {}, str runName = ""){
     TTL ttlProgram = [TTL] "";
     
     map[tuple[str, loc], list[Message]]failedTests = ();
@@ -100,12 +100,14 @@ bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t) getModel, b
                 continue;
             }
             ntests += 1;
+            newTreeSrc = |unknown:///|;
             try {
               newTree = visit(parse(begin, "<ti.tokens>")) {
                 case Tree t => t[src = relocate(t.src, ti.tokens.src)]
                     when t has src
               };
-              model = getModel(newTree);
+              newTreeSrc = newTree.src;
+              model = getModel(newTree, "<ti.name>");
               list[Message] messages = model.messages;
               if(verbose) println("runTests: <messages>");
               expected = ti.expect is none ? {} : {deescape("<s>"[1..-1]) | TTL_String s <- ti.expect.messages};
@@ -118,7 +120,9 @@ bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t) getModel, b
                 failedTests[<"<ti.name>", suite>]  = [error("Parse error", relocate(l, ti.tokens.src))];
            } catch Ambiguity(loc l, nt, inp): {
                 failedTests[<"<ti.name>", suite>]  = [error("Ambiguity (<nt> on `<inp>`)", (l.offset?) ? relocate(l, ti.tokens.src) : l)];
-           } 
+           } catch AssertionFailed(str s): {
+                failedTests[<"<ti.name>", suite>]  = [error("Assertion failed: <s>", newTreeSrc)];
+           }
 
         }
         testTime += (cpuTime() - startTests);
@@ -143,7 +147,7 @@ bool runTests(list[loc] suites, type[&T<:Tree] begin, TModel(Tree t) getModel, b
         }
     }
     println("Parse time: <parseTime/1000000> msec; Test time: <testTime/1000000> msec");
-    return ok;
+    return ok && isEmpty(failedTests);
 }
 
 lrel[&T<:Tree, set[str]] extractTests(list[loc] suites, type[&T<:Tree] begin) {
diff --git a/src/examples/aliases/Test.rsc b/src/examples/aliases/Test.rsc
index 4821debd..b12d2d08 100644
--- a/src/examples/aliases/Test.rsc
+++ b/src/examples/aliases/Test.rsc
@@ -20,8 +20,8 @@ import ParseTree;
 
 // ---- Testing ---------------------------------------------------------------
 
-TModel aliasesTModelForTree(Tree pt){
-    return collectAndSolve(pt, config = aliasesConfig(), modelName = "alias");
+TModel aliasesTModelForTree(Tree pt, bool assertValidUseDef = true){
+    return collectAndSolve(pt, config = aliasesConfig()[assertValidDefines = true][assertValidUseDef = assertValidUseDef], modelName = "alias");
 }
 
 TModel aliasesTModelFromName(str mname){
@@ -32,7 +32,10 @@ TModel aliasesTModelFromName(str mname){
 test bool aliasesTests() {
     return runTests([|project://typepal/src/examples/aliases/aliases.ttl|], 
                     #start[Program], 
-                    TModel (Tree t) { return aliasesTModelForTree(t); },
+                    // Enable `assertValidUseDef` only when the program under
+                    // test **isn't** `CircularAlias1` (which is expected to
+                    // have an invalid `useDef`).
+                    TModel (Tree t, str name) { return aliasesTModelForTree(t, assertValidUseDef = name != "CircularAlias1"); },
                     runName = "Aliases");
 }
 
diff --git a/src/examples/calc/Test.rsc b/src/examples/calc/Test.rsc
index c6c4396e..885fe3e1 100644
--- a/src/examples/calc/Test.rsc
+++ b/src/examples/calc/Test.rsc
@@ -21,7 +21,7 @@ import ParseTree;                           // In order to parse tests
 // ---- Testing ---------------------------------------------------------------
 
 TModel calcTModelForTree(Tree pt){
-    return collectAndSolve(pt, modelName = "calc");
+    return collectAndSolve(pt, modelName = "calc", config = tconfig()[assertValidDefines = true][assertValidUseDef = true]);
 }
 
 TModel calcTModelFromStr(str text){
@@ -32,7 +32,7 @@ TModel calcTModelFromStr(str text){
 test bool calcTests() {
      return runTests([|project://typepal/src/examples/calc/tests.ttl|], 
                      #Calc, 
-                     calcTModelForTree, 
+                     TModel (Tree t, str _name) { return calcTModelForTree(t); },
                      runName="Calc");
 }
 
diff --git a/src/examples/dataModel/Test.rsc b/src/examples/dataModel/Test.rsc
index a002a76d..c958bf8d 100644
--- a/src/examples/dataModel/Test.rsc
+++ b/src/examples/dataModel/Test.rsc
@@ -17,7 +17,7 @@ extend examples::dataModel::Checker;
 extend analysis::typepal::TestFramework;
 
 TModel dmTModelForTree(Tree pt){
-    return collectAndSolve(pt, config = dmConfig());
+    return collectAndSolve(pt, config = dmConfig()[assertValidDefines = true][assertValidUseDef = true]);
 }
 
 TModel dmTModelFromName(str mname){
diff --git a/src/examples/evenOdd/Test.rsc b/src/examples/evenOdd/Test.rsc
index 9803c305..db460ab9 100644
--- a/src/examples/evenOdd/Test.rsc
+++ b/src/examples/evenOdd/Test.rsc
@@ -23,7 +23,7 @@ import ParseTree;                           // In order to parse tests
 
 TModel evenOddTModelForTree(Tree pt){
     if(pt has top) pt = pt.top;
-    c = newCollector("even-odd", pt,  tconfig());
+    c = newCollector("even-odd", pt, tconfig()[assertValidDefines = true][assertValidUseDef = true]);
     collect(pt, c);
     return newSolver(pt, c.run()).run();
 }
@@ -36,7 +36,7 @@ TModel evenOddTModelFromStr(str text){
 test bool evenOddTests() {
      return runTests([|project://typepal/src/examples/evenOdd/tests.ttl|], 
                      #EvenOdd, 
-                     evenOddTModelForTree, 
+                     TModel (Tree t, str _name) { return evenOddTModelForTree(t); },
                      runName="EvenOdd");
 }
 
diff --git a/src/examples/fixedMembers/Test.rsc b/src/examples/fixedMembers/Test.rsc
index 6cd83544..fd5fe483 100644
--- a/src/examples/fixedMembers/Test.rsc
+++ b/src/examples/fixedMembers/Test.rsc
@@ -22,7 +22,7 @@ import ParseTree;
 // ---- Testing ---------------------------------------------------------------
 
 TModel fixedMembersTModelForTree(Tree pt){
-    return collectAndSolve(pt, config = fixedMembersConfig(), modelName="fixed-members");
+    return collectAndSolve(pt, config = fixedMembersConfig()[assertValidDefines = true][assertValidUseDef = true], modelName = "fixed-members");
 }
 
 TModel fixedMembersTModelFromName(str mname){
@@ -33,7 +33,7 @@ TModel fixedMembersTModelFromName(str mname){
 test bool fixedMembersTests() {
     return runTests([|project://typepal/src/examples/fixedMembers/fixedMembers.ttl|], 
                     #start[Program], 
-                    TModel (Tree t) { return fixedMembersTModelForTree(t); },
+                    TModel (Tree t, str _name) { return fixedMembersTModelForTree(t); },
                     runName = "fixedMembers");
 }
 
diff --git a/src/examples/fun/Test.rsc b/src/examples/fun/Test.rsc
index bb8978ae..5241e4a2 100644
--- a/src/examples/fun/Test.rsc
+++ b/src/examples/fun/Test.rsc
@@ -27,7 +27,7 @@ TModel funTModel(str name){
 }
 
 TModel funTModelForTree(Tree pt){
-    return collectAndSolve(pt, modelName = "fun");
+    return collectAndSolve(pt, modelName = "fun", config = tconfig()[assertValidDefines = true][assertValidUseDef = true]);
 }
 
 TModel funTModelFromStr(str text){
@@ -41,6 +41,12 @@ list[Message] funCheck(str name) {
 }
 
 test bool funTests() 
-    =  runTests([|project://typepal/src/examples/fun/tests.ttl|], #Fun, funTModelForTree, runName="Fun");
+    = runTests([|project://typepal/src/examples/fun/tests.ttl|],
+                #Fun,
+                TModel (Tree t, str _name) { return funTModelForTree(t); },
+                runName="Fun");
+
+test bool funTModelTestBig() = [] := funTModel("big").messages;
+test bool funTModelTestTmp() = [] := funTModel("tmp").messages;
 
 value main() = funTests();
diff --git a/src/examples/fwjava/Test.rsc b/src/examples/fwjava/Test.rsc
index 741791e9..e62bfe4b 100644
--- a/src/examples/fwjava/Test.rsc
+++ b/src/examples/fwjava/Test.rsc
@@ -23,7 +23,7 @@ import ParseTree;
 TModel fwjTModelForTree(Tree pt){
     if(pt has top) pt = pt.top;
     
-    c = newCollector("fwj", pt, fwjConfig());
+    c = newCollector("fwj", pt, fwjConfig()[assertValidDefines = true][assertValidUseDef = true]);
     fwjPreCollectInitialization(pt, c);
     collect(pt, c);
     return newSolver(pt, c.run()).run();
@@ -37,8 +37,18 @@ TModel fwjTModelFromName(str mname, bool _){
 test bool fwjTests() {
     return runTests([|project://typepal/src/examples/fwjava/tests.ttl|], 
                      #start[FWJProgram], 
-                     TModel (Tree t) { return fwjTModelForTree(t); },
+                     TModel (Tree t, str _name) { return fwjTModelForTree(t); },
                      runName = "FwJava");
 }
 
+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);
+    return true;
+}
+
 value main() = fwjTests();
\ No newline at end of file
diff --git a/src/examples/modfun/A.mfun b/src/examples/modfun/A.mfun
index 144382ad..6085491f 100644
--- a/src/examples/modfun/A.mfun
+++ b/src/examples/modfun/A.mfun
@@ -2,4 +2,4 @@ module A {
     import B;
     def a : int -> int = fun i : int { 5 + i };
     def a : int -> int = fun i : int { 6 + i };
-}
+}
\ No newline at end of file
diff --git a/src/examples/modfun/Test.rsc b/src/examples/modfun/Test.rsc
index 3bce6cd1..591fe5e4 100644
--- a/src/examples/modfun/Test.rsc
+++ b/src/examples/modfun/Test.rsc
@@ -28,7 +28,7 @@ TModel modfunTModel(str name){
 }
 
 TModel modfunTModelForTree(Tree pt){
-    return collectAndSolve(pt, modelName="modfun");
+    return collectAndSolve(pt, modelName="modfun", config=tconfig()[assertValidDefines=true][assertValidUseDef=true]);
 }
 
 TModel modfunTModelFromStr(str text){
@@ -43,9 +43,13 @@ list[Message] modfunCheck(str name) {
 
 test bool modfunTests()
     = runTests([|project://typepal/src/examples/modfun/tests.ttl|], 
-               #ModFun,
-               modfunTModelForTree,
-               runName = "ModFun");
+                #ModFun,
+                TModel (Tree t, str _name) { return modfunTModelForTree(t); },
+                runName = "ModFun");
+
+test bool modfunTModelTestA() = [_, _, _] := modfunTModel("A").messages; // Three errors expected
+test bool modfunTModelTestB() = [_, _] := modfunTModel("B").messages; // Two errors expected
+test bool modfunTModelTestTmp() = [] := modfunTModel("tmp").messages;
 
 value main() 
     =  modfunTests();
\ No newline at end of file
diff --git a/src/examples/modules/Checker.rsc b/src/examples/modules/Checker.rsc
index 400d7bc3..689fc01b 100644
--- a/src/examples/modules/Checker.rsc
+++ b/src/examples/modules/Checker.rsc
@@ -147,7 +147,7 @@ list[Message] runModules(str name, bool debug = false) {
 }
  
 bool testModules(int n, bool debug = false, set[str] runOnly = {}) {
-    return runTests([|project://modules-core/src/lang/modules/modules<"<n>">.ttl|], #start[Program], TModel (Tree t) {
+    return runTests([|project://modules-core/src/lang/modules/modules<"<n>">.ttl|], #start[Program], TModel (Tree t, str _name) {
         return modulesTModelFromTree(t);
     }, runOnly = runOnly);
 }
diff --git a/src/examples/pascal/Test.rsc b/src/examples/pascal/Test.rsc
index 6828589d..ec3f1133 100644
--- a/src/examples/pascal/Test.rsc
+++ b/src/examples/pascal/Test.rsc
@@ -26,7 +26,7 @@ import util::Reflective;
 TModel pascalTModelForTree(Tree pt, str programName, PathConfig _, bool _){
     if(pt has top) pt = pt.top;
     
-    c = newCollector(programName, pt, pascalConfig());
+    c = newCollector(programName, pt, pascalConfig()[assertValidDefines = true][assertValidUseDef = true]);
     pascalPreCollectInitialization(pt, c);
     collect(pt, c);
     return newSolver(pt, c.run()).run();
@@ -35,7 +35,7 @@ TModel pascalTModelForTree(Tree pt, str programName, PathConfig _, bool _){
 TModel pascalTModelForTree(Tree pt, bool _){
     if(pt has top) pt = pt.top;
     
-    c = newCollector("pascal", pt, pascalConfig());
+    c = newCollector("pascal", pt, pascalConfig()[assertValidDefines = true][assertValidUseDef = true]);
     pascalPreCollectInitialization(pt, c);
     collect(pt, c);
     return newSolver(pt, c.run()).run();
@@ -57,7 +57,7 @@ test bool pascalTests() {
     //return true;
     bool ok = runTests([|project://typepal/src/examples/pascal/expression-tests.ttl|,
                         |project://typepal/src/examples/pascal/statement-tests.ttl|
-                       ], #start[Program], TModel (Tree t) { return pascalTModelForTree(t, false); },
+                       ], #start[Program], TModel (Tree t, str _name) { return pascalTModelForTree(t, false); },
                        runName = "Pascal");
     println("Executing Pascal examples\r");
     int n = 0;
diff --git a/src/examples/pico/Test.rsc b/src/examples/pico/Test.rsc
index 06cf78e3..d31cea23 100644
--- a/src/examples/pico/Test.rsc
+++ b/src/examples/pico/Test.rsc
@@ -22,19 +22,21 @@ import ParseTree;
 
 TModel picoTModelFromName(str name) {
     Tree pt = parse(#start[Program], |project://typepal/src/examples/pico/<name>.pico|);
-    return collectAndSolve(pt, modelName="pico");
+    return collectAndSolve(pt, modelName="pico", config=tconfig()[assertValidDefines=true][assertValidUseDef=true]);
 }
 
 TModel picoTModelForTree(Tree pt) {
-    return collectAndSolve(pt, modelName="pico");
+    return collectAndSolve(pt, modelName="pico", config=tconfig()[assertValidDefines=true][assertValidUseDef=true]);
 }
 
 test bool picoTests() {
     return runTests([|project://typepal/src/examples/pico/tests.ttl|], 
                     #start[Program], 
-                    TModel (Tree t) { return picoTModelForTree(t); },
+                    TModel (Tree t, str _name) { return picoTModelForTree(t); },
                     runName = "Pico");
 }
 
+test bool picoTModelTestFac() = [] := picoTModelFromName("fac").messages;
+
 value main()
     = picoTests();
\ No newline at end of file
diff --git a/src/examples/ql/Test.rsc b/src/examples/ql/Test.rsc
index 9a290f1c..4bb94016 100644
--- a/src/examples/ql/Test.rsc
+++ b/src/examples/ql/Test.rsc
@@ -22,18 +22,23 @@ import ParseTree;
 
 TModel qlTModelForName(str name) {
     Tree pt = parse(#start[Form], |project://typepal/src/examples/ql/examples/<name>.ql|);
-    return collectAndSolve(pt, modelName = "ql");
+    return collectAndSolve(pt, modelName = "ql", config = tconfig()[assertValidDefines = true][assertValidUseDef = true]);
 }
 
 TModel qlTModelForTree(Tree pt) {
-    return collectAndSolve(pt, modelName = "ql");
+    return collectAndSolve(pt, modelName = "ql", config = tconfig()[assertValidDefines = true][assertValidUseDef = true]);
 }
 
 test bool qlTests() {
     return runTests([|project://typepal/src/examples/ql/tests.ttl|], #start[Form], 
-                     TModel (Tree t) { return qlTModelForTree(t); },
+                     TModel (Tree t, str _name) { return qlTModelForTree(t); },
                      runName = "QL");
 }
 
+test bool qlTModelTestAddition() = [] := qlTModelForName("addition").messages;
+test bool qlTModelTestAvg() = [] := qlTModelForName("avg").messages;
+test bool qlTModelTestTax() = [] := qlTModelForName("tax").messages;
+test bool qlTModelTestTax2() = [] := qlTModelForName("tax2").messages;
+
 value main()
     = qlTests();
\ No newline at end of file
diff --git a/src/examples/smallOO/Test.rsc b/src/examples/smallOO/Test.rsc
index 1259298b..7c0d3c9d 100644
--- a/src/examples/smallOO/Test.rsc
+++ b/src/examples/smallOO/Test.rsc
@@ -21,7 +21,7 @@ import ParseTree;
 // ---- Testing ---------------------------------------------------------------
                
 TModel smallOOTModelForTree(Tree pt){
-    return collectAndSolve(pt, config=smallConfig(), modelName="smalloo");
+    return collectAndSolve(pt, config=smallConfig()[assertValidDefines=true][assertValidUseDef=true], modelName="smalloo");
 }
 
 TModel smallOOTModelFromName(str mname){
@@ -36,9 +36,12 @@ list[Message] checkSmallOO(str mname) {
 test bool smallOOTests() {
     return runTests([|project://typepal/src/examples/smallOO/tests.ttl|], 
                     #start[Module], 
-                    TModel (Tree t) { return smallOOTModelForTree(t); },
+                    TModel (Tree t, str _name) { return smallOOTModelForTree(t); },
                     runName = "SmallOO");
 }
 
+test bool smallOOTModelTestM1() = [_] := smallOOTModelFromName("M1").messages;  // One error expected
+test bool smallOOTModelTestM2() = [] := smallOOTModelFromName("M2").messages;
+
 value main()
     = smallOOTests();
\ No newline at end of file
diff --git a/src/examples/splitstruct/Test.rsc b/src/examples/splitstruct/Test.rsc
index dc47fea0..11fa56d8 100644
--- a/src/examples/splitstruct/Test.rsc
+++ b/src/examples/splitstruct/Test.rsc
@@ -22,7 +22,7 @@ import ParseTree;
 // ---- Testing ---------------------------------------------------------------
 
 TModel splitstructTModelForTree(Tree pt){
-    return collectAndSolve(pt, config = splitstructConfig(), modelName="splitstruct");
+    return collectAndSolve(pt, config = splitstructConfig()[assertValidDefines = true][assertValidUseDef = true], modelName = "splitstruct");
 }
 
 TModel splitstructTModelFromName(str mname){
@@ -33,7 +33,7 @@ TModel splitstructTModelFromName(str mname){
 test bool splitstructTests() {
     return runTests([|project://typepal/src/examples/splitstruct/tests.ttl|], 
                     #start[Program],
-                    TModel (Tree t) { return splitstructTModelForTree(t); },
+                    TModel (Tree t, str _name) { return splitstructTModelForTree(t); },
                     runName = "SplitStruct");
 }
 
diff --git a/src/examples/staticFields/Test.rsc b/src/examples/staticFields/Test.rsc
index 0ec96dec..39fbde58 100644
--- a/src/examples/staticFields/Test.rsc
+++ b/src/examples/staticFields/Test.rsc
@@ -22,7 +22,7 @@ import ParseTree;
 // ---- Testing ---------------------------------------------------------------
 
 TModel staticFieldsTModelForTree(Tree pt){
-    return collectAndSolve(pt, config=staticFieldsConfig(), modelName="staticfields");
+    return collectAndSolve(pt, config=staticFieldsConfig()[assertValidDefines=true][assertValidUseDef=true], modelName="staticfields");
 }
 
 TModel staticFieldsTModelFromName(str mname){
@@ -33,7 +33,7 @@ TModel staticFieldsTModelFromName(str mname){
 test bool staticFieldsTests() {
     return runTests([|project://typepal/src/examples/staticFields/tests.ttl|], 
                     #start[Program], 
-                    TModel (Tree t) { return staticFieldsTModelForTree(t); },
+                    TModel (Tree t, str _name) { return staticFieldsTModelForTree(t); },
                     runName = "StaticFields");
 }
 
diff --git a/src/examples/struct/Test.rsc b/src/examples/struct/Test.rsc
index f7be6807..3bf42ebb 100644
--- a/src/examples/struct/Test.rsc
+++ b/src/examples/struct/Test.rsc
@@ -22,7 +22,7 @@ import ParseTree;
 // ---- Testing ---------------------------------------------------------------
 
 TModel structTModelForTree(Tree pt){
-    return collectAndSolve(pt, config = structConfig(), modelName="struct");
+    return collectAndSolve(pt, config = structConfig()[assertValidDefines = true][assertValidUseDef = true], modelName = "struct");
 }
 
 TModel structTModelFromName(str mname){
@@ -33,7 +33,7 @@ TModel structTModelFromName(str mname){
 test bool structTests() {
     return runTests([|project://typepal/src/examples/struct/tests.ttl|], 
                     #start[Program],
-                    TModel (Tree t) { return structTModelForTree(t); },
+                    TModel (Tree t, str _name) { return structTModelForTree(t); },
                     runName = "Struct");
 }
 
diff --git a/src/examples/structParameters/Test.rsc b/src/examples/structParameters/Test.rsc
index 1b9a4fc3..4777cfa2 100644
--- a/src/examples/structParameters/Test.rsc
+++ b/src/examples/structParameters/Test.rsc
@@ -22,7 +22,7 @@ import ParseTree;
 // ---- Testing ---------------------------------------------------------------
 
 TModel structParametersTModelForTree(Tree pt){
-    return collectAndSolve(pt, config = structParametersConfig(), modelName="struct-parameters");
+    return collectAndSolve(pt, config = structParametersConfig()[assertValidDefines = true][assertValidUseDef = true], modelName = "struct-parameters");
 }
 
 TModel structParametersTModelFromName(str mname){
@@ -33,9 +33,11 @@ TModel structParametersTModelFromName(str mname){
 test bool structParametersTests() {
     return runTests([|project://typepal/src/examples/structParameters/tests.ttl|], 
                      #start[Program], 
-                     TModel (Tree t) { return structParametersTModelForTree(t); },
+                     TModel (Tree t, str _name) { return structParametersTModelForTree(t); },
                      runName = "StructParameters");
 }
 
+test bool structParametersTModelTestTmp() = [] := structParametersTModelFromName("Tmp").messages;
+
 value main()
     = structParametersTests();
\ No newline at end of file
diff --git a/src/examples/untypedFun/Test.rsc b/src/examples/untypedFun/Test.rsc
index b93524ac..020a0285 100644
--- a/src/examples/untypedFun/Test.rsc
+++ b/src/examples/untypedFun/Test.rsc
@@ -26,9 +26,15 @@ list[Message] untypedFunCheck(str name){
 }
 
 TModel untypedFunTModelForTree(Tree pt)
-    = collectAndSolve(pt, modelName="ufun");
+    = collectAndSolve(pt, modelName="ufun", config=tconfig()[assertValidDefines=true][assertValidUseDef=true]);
 
 test bool untypedFunTests()
-    = runTests([|project://typepal/src/examples/untypedFun/tests.ttl|], #Expression, untypedFunTModelForTree, runName="UntypedFun");
+    = runTests([|project://typepal/src/examples/untypedFun/tests.ttl|],
+                #Expression,
+                TModel (Tree t, str _name) { return untypedFunTModelForTree(t); },
+                runName="UntypedFun");
+
+test bool untypedFunTModelTestBig() = [] := untypedFunTModelForTree(sample("big")).messages;
+test bool untypedFunTModelTestTmp() = [_] := untypedFunTModelForTree(sample("tmp")).messages; // One error expected
 
 value main() = untypedFunTests();