diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 96ff23d0a487b4007fc07cd533f094556dbf4169..a23de525f478cf78e8ddf450db2a83af7b63fb9b 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -1,10 +1,11 @@
 name: CI
 
 on:
+  workflow_dispatch:
   push:
     # Sequence of patterns matched against refs/heads
     branches:    
-      - v1.7.2         # Push events on master branch
+      - v1.7.3         # Push events on master branch
 
 jobs:
 
@@ -16,8 +17,8 @@ jobs:
         include: 
         - operating-system: ubuntu-latest
           MVN_COMMAND: xvfb-run mvn -Dtest.skip=true -Dmaven.test.failure.ignore=true 
-          GITHUB_RELEASE_NAME: The Theano release
-          TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.7.2-linux.gtk.x86_64.zip
+          GITHUB_RELEASE_NAME: The Ulpian release
+          TOOLBOX_PRODUCT_ZIP: TLAToolbox-1.7.3-linux.gtk.x86_64.zip
 
     steps:
 
@@ -75,12 +76,12 @@ jobs:
            ## Generate changelog
            cd general/docs/changelogs
            ## Append sha1 sum to changelog (last line of changelog has the table header).
-           echo "$(sha1sum ../../../tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar"  >> ch1_7_2.md
+           echo "$(sha1sum ../../../tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar"  >> ch1_7_3.md
            ## Two above as one-liner without intermediate file.
-           $(jq -n --argjson changelog "$(cat ch1_7_2.md | jq  --raw-input --slurp .)" -f gh-1_7_2.jq > gh-1_7_2.json)
+           $(jq -n --argjson changelog "$(cat ch1_7_3.md | jq  --raw-input --slurp .)" -f gh-1_7_3.jq > gh-1_7_3.json)
            ## Update draft release with latest changelog in case it changed.
            ## https://developer.github.com/v3/repos/releases/#edit-a-release
-           curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE -d @gh-1_7_2.json -X PATCH --header "Content-Type: application/json"
+           curl -sS -H "Authorization: token ${{secrets.GITHUB_TOKEN}}" https://api.github.com/repos/${{ github.repository }}/releases/$DRAFT_RELEASE -d @gh-1_7_3.json -X PATCH --header "Content-Type: application/json"
 
     ## 
     ## Update all git tags to make the download urls work, i.e.
diff --git a/.jenkins.groovy b/.jenkins.groovy
index 5ca9fabaf89a34cfed99379c5e607fda966cd66f..bf56195d4f44ece0b14aa994f92cb7244cbfbfc0 100644
--- a/.jenkins.groovy
+++ b/.jenkins.groovy
@@ -46,7 +46,7 @@ for (x in labels) {
 		      }
 	   	      // the macosx zip on the master node to have it signed with the Apple certificate on macosx.  However, only master
 		      // has the lamport certificate to sign the individual toolbox bundles.
-		      stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip', name: 'toolbox'
+		      stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.3-macosx.cocoa.x86_64.zip', name: 'toolbox'
                     } else {
 			  withMaven(
 			    // Maven installation declared in the Jenkins "Global Tool Configuration"
@@ -153,7 +153,7 @@ node ('master') {
    }
    
    stage('RenderChangelog') { // Render the github flavord markdown to html
-       sh 'grip --context=tlaplus/tlaplus --export ${WORKSPACE}/general/docs/changelogs/ch1_7_1.md ${WORKSPACE}/general/docs/changelogs/changelog.html'
+       sh 'grip --context=tlaplus/tlaplus --export ${WORKSPACE}/general/docs/changelogs/ch1_7_3.md ${WORKSPACE}/general/docs/changelogs/changelog.html'
    }
 }
 
@@ -162,11 +162,11 @@ node ('macos') {
         sh 'rm -rf *'
         unstash 'toolbox'
         sh 'ls -lah'
-        sh 'unzip toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip'
+        sh 'unzip toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.3-macosx.cocoa.x86_64.zip'
         sh 'codesign -f -s "Developer ID Application: M K (3PCM4M3RWK)" -v "TLA+ Toolbox.app" --deep'
-        sh 'ditto -ck --sequesterRsrc --keepParent "TLA+ Toolbox.app" TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip'
-        sh 'mv TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip toolbox/org.lamport.tla.toolbox.product.product/target/products/'
-        stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip', name: 'signed'
+        sh 'ditto -ck --sequesterRsrc --keepParent "TLA+ Toolbox.app" TLAToolbox-1.7.3-macosx.cocoa.x86_64.zip'
+        sh 'mv TLAToolbox-1.7.3-macosx.cocoa.x86_64.zip toolbox/org.lamport.tla.toolbox.product.product/target/products/'
+        stash includes: 'toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.3-macosx.cocoa.x86_64.zip', name: 'signed'
     }
 }
 
@@ -188,13 +188,13 @@ node ('master') {
            cd ${WORKSPACE}/general/docs/changelogs
 
            ## Append sha1 sum to changelog (last line of changelog has the table header).
-           echo "$(sha1sum ${WORKSPACE}/tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar"  >> ch1_7_1.md
-           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-win32.win32.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.1-win32.win32.x86_64.zip" >> ch1_7_1.md
-           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip" >> ch1_7_1.md     
-           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-linux.gtk.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.1-linux.gtk.x86_64.zip" >> ch1_7_1.md
+           echo "$(sha1sum ${WORKSPACE}/tlatools/org.lamport.tlatools/dist/tla2tools.jar | cut -f 1 -d " ")|tla2tools.jar"  >> ch1_7_3.md
+           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.3-win32.win32.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.3-win32.win32.x86_64.zip" >> ch1_7_3.md
+           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.3-macosx.cocoa.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.3-macosx.cocoa.x86_64.zip" >> ch1_7_3.md     
+           echo "$(sha1sum ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.3-linux.gtk.x86_64.zip | cut -f 1 -d " ")|TLAToolbox-1.7.3-linux.gtk.x86_64.zip" >> ch1_7_3.md
            
            ## Two above as one-liner without intermediate file.
-           $(jq -n --argjson changelog "$(cat ch1_7_1.md | jq  --raw-input --slurp .)" -f gh-1_7_1.jq > gh-1_7_1.json)
+           $(jq -n --argjson changelog "$(cat ch1_7_3.md | jq  --raw-input --slurp .)" -f gh-1_7_3.jq > gh-1_7_3.json)
 
            ## Get id of existing draft release with given name.
            DRAFT_RELEASE=$(curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases --header "Content-Type: application/json" | jq '.[]| select(.draft==true and .name=="The Brontinus release") | .id')
@@ -202,7 +202,7 @@ node ('master') {
 
            ## Update draft release with latest changelog in case it changed.
            ## https://developer.github.com/v3/repos/releases/#edit-a-release
-           curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE -d @gh-1_7_1.json -X PATCH --header "Content-Type: application/json"
+           curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE -d @gh-1_7_3.json -X PATCH --header "Content-Type: application/json"
 
            ## Remove old assets otherwise upload below will error.
            ASSETS=$(curl -sS -H "Authorization: token ${GITHUB_TOKEN}" https://api.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets --header "Content-Type: application/json" | jq '.[]| .id')
@@ -216,15 +216,15 @@ node ('master') {
             ## tla2tools.jar
             curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=tla2tools.jar --upload-file ${WORKSPACE}/tlatools/org.lamport.tlatools/dist/tla2tools.jar
             ## macOS
-            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-macosx.cocoa.x86_64.zip
+            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.3-macosx.cocoa.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.3-macosx.cocoa.x86_64.zip
             ## win32
-            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-win32.win32.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-win32.win32.x86_64.zip
+            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.3-win32.win32.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.3-win32.win32.x86_64.zip
             ## Linux
-            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-linux.gtk.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.1-linux.gtk.x86_64.zip
+            curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.3-linux.gtk.x86_64.zip --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLAToolbox-1.7.3-linux.gtk.x86_64.zip
             ## deb
-            #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-linux.gtk.amd64.deb --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/repository/TLAToolbox-1.7.1-linux.gtk.amd64.deb
+            #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.3-linux.gtk.amd64.deb --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/repository/TLAToolbox-1.7.3-linux.gtk.amd64.deb
             ## RPM
-            #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.1-linux.gtk.amd64.rpm --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLA\\+Toolbox-1.7.1~*.x86_64.rpm
+            #curl -s -X POST -H "Content-Type: application/zip" -H "Authorization: token ${GITHUB_TOKEN}" https://uploads.github.com/repos/tlaplus/tlaplus/releases/$DRAFT_RELEASE/assets?name=TLAToolbox-1.7.3-linux.gtk.amd64.rpm --upload-file ${WORKSPACE}/toolbox/org.lamport.tla.toolbox.product.product/target/products/TLA\\+Toolbox-1.7.3~*.x86_64.rpm
          '''
         }
    }
diff --git a/general/docs/changelogs/ch1_7_3.md b/general/docs/changelogs/ch1_7_3.md
new file mode 100644
index 0000000000000000000000000000000000000000..9ecb87ddc131739bac13b403ff7f776e8733001f
--- /dev/null
+++ b/general/docs/changelogs/ch1_7_3.md
@@ -0,0 +1,8 @@
+The [Ulpian](https://en.wikipedia.org/wiki/Ulpian) release is based on the [1.7.3 branch](https://github.com/tlaplus/tlaplus/releases/tag/v1.7.3) and fixes the issue below.
+
+### Changelog
+* [LazyValue can cause TLC to generate too many or too few states](https://github.com/tlaplus/tlaplus/issues/798)
+
+### Checksums
+sha1sum|file
+------------ | -------------
\ No newline at end of file
diff --git a/general/docs/changelogs/gh-1_7_3.jq b/general/docs/changelogs/gh-1_7_3.jq
new file mode 100644
index 0000000000000000000000000000000000000000..d0026f4922879502dd99b7639cb98ad64a3f01a1
--- /dev/null
+++ b/general/docs/changelogs/gh-1_7_3.jq
@@ -0,0 +1,7 @@
+{
+  "tag_name": "v1.7.3",
+  "name": "The Ulpian release",
+  "draft": true,
+  "prerelease": false,
+  "body": $changelog
+}
\ No newline at end of file
diff --git a/pom.xml b/pom.xml
index 801dfde2289aef3fd078e8d5e707c13d800dfbfe..ef6b5af4e8022a17e99f53f3ae1df1f89f61af5b 100644
--- a/pom.xml
+++ b/pom.xml
@@ -123,7 +123,7 @@
 		<!-- Align toolbox.version with the version in
 			 org.lamport.tla.toolbox.product.product.product
 			 product.version. -->
-		<toolbox.version>1.7.1</toolbox.version>
+		<toolbox.version>1.7.3</toolbox.version>
 
 		<!-- This is used in org.lamport.tla.toolbox.product.uitest but
 			has been placed at the top level should it need be referenced
diff --git a/tlatools/org.lamport.tlatools/github.xml b/tlatools/org.lamport.tlatools/github.xml
index 098473a97da955fa58de84c7b7193a6fe4237c8a..141044f3086b7f14a12392cb2746a6cab4c90349 100644
--- a/tlatools/org.lamport.tlatools/github.xml
+++ b/tlatools/org.lamport.tlatools/github.xml
@@ -10,7 +10,7 @@
 	<groupId>org.lamport</groupId>
 	<artifactId>tla2tools</artifactId>
 	<name>TLA+ Tools</name>
-	<version>1.7.2-SNAPSHOT</version>
+	<version>1.7.3-SNAPSHOT</version>
 	<description>The TLC model checker, the syntax and semantic checker SANY, the PlusCal translator, and the LaTeX pretty printer.</description>
 	<packaging>jar</packaging>
 
diff --git a/tlatools/org.lamport.tlatools/ossrh.xml b/tlatools/org.lamport.tlatools/ossrh.xml
index f6f7a40e38d059bc777c43a5f0ff1beddb4fc3c4..b4cc5f211b66247c9af45228d363b41ee17b0624 100644
--- a/tlatools/org.lamport.tlatools/ossrh.xml
+++ b/tlatools/org.lamport.tlatools/ossrh.xml
@@ -17,7 +17,7 @@
 	<groupId>org.lamport</groupId>
 	<artifactId>tla2tools</artifactId>
 	<name>TLA+ Tools</name>
-	<version>1.7.1-SNAPSHOT</version>
+	<version>1.7.3-SNAPSHOT</version>
 	<description>The TLC model checker, the syntax and semantic checker SANY, the PlusCal translator, and the LaTeX pretty printer.</description>
 	<packaging>jar</packaging>
 
diff --git a/tlatools/org.lamport.tlatools/pom.xml b/tlatools/org.lamport.tlatools/pom.xml
index f2c1f1eaddacb99f31077d6a5243ea87aa269821..924f664036cebd2b05aa49e27faf9aa9ab1af4b8 100644
--- a/tlatools/org.lamport.tlatools/pom.xml
+++ b/tlatools/org.lamport.tlatools/pom.xml
@@ -194,7 +194,7 @@
 	<dependency>
 		<groupId>org.apache.ant</groupId>
 		<artifactId>ant-junit</artifactId>
-		<version>1.7.1</version>
+		<version>1.7.3</version>
 		<scope>compile</scope>
 	</dependency>
   		<dependency>
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java b/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java
index d821d03a0ef3a2a050867b6d3a0a6bf134785357..d88c46c664dd603e0ea539423293c045540d6ad1 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/TLCGlobals.java
@@ -23,7 +23,7 @@ public class TLCGlobals
 	public static final int DEFAULT_CHECKPOINT_DURATION = (30 * 60 * 1000) + 42;
 
 	// The current version of TLC
-    public static String versionOfTLC = "Version 2.17 of 02 February 2022";
+    public static String versionOfTLC = "Version 2.18 of 20 March 2023";
     
     // The bound for set enumeration, used for pretty printing
     public static int enumBound = 2000;
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/SymbolNodeValueLookupProvider.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/SymbolNodeValueLookupProvider.java
index 361ba9c32712a4a76c195faea0e5e489399b3015..e56b9b850d2ebfab196cae52f7c0481999cbe9b0 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/SymbolNodeValueLookupProvider.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/SymbolNodeValueLookupProvider.java
@@ -87,6 +87,18 @@ public interface SymbolNodeValueLookupProvider {
 	}
 
 	default Object getVal(final ExprOrOpArgNode expr, final Context c, final boolean cachable, final CostModel cm, final int forToolId) {
+		if (!LazyValue.LAZYEVAL_OFF && expr instanceof OpApplNode) {
+			final OpApplNode oan = (OpApplNode) expr;
+			// Do not create a LazyValue that "points to" another LazyValue.
+			// Related:
+			// https://github.com/tlaplus/tlaplus/issues/113
+			// https://github.com/tlaplus/tlaplus/issues/798
+			final Object l = c.lookup(oan.getOperator());
+			if (l instanceof LazyValue) {
+				return l;
+			}
+			return new LazyValue(expr, c, cachable, cm);
+		}
 		if (expr instanceof ExprNode) {
 			return new LazyValue(expr, c, cachable, cm);
 		}
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
index d2c2030a45df281d9a03039afd5e4c2ccb7090b2..21f0d18e5708e86e95f218ae1f36b297599b9ade 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
@@ -1554,7 +1554,7 @@ public abstract class Tool
 						// (https://github.com/tlaplus/tlaplus/issues/113) - 
 						// TLC can generate invalid sets of init or next-states caused by broken
 						// LazyValue evaluation. The related tests are AssignmentInit* and
-						// AssignmentNext*. Without this fix TLC essentially reuses a stale lv.val when
+						// AssignmentNext*. Without this fix, TLC essentially reuses a stale lv.val when
 						// it needs to re-evaluate res because the actual operands to eval changed.
 						// Below is Leslie's formal description of the bug:
 						// 
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java b/tlatools/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java
index 81ee51d9413883138c546f34d4be4bfb2ea95db9..fe5b1eba3978c9fecdc5ca4e5c9b064a343762c3 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java
@@ -29,7 +29,7 @@ public class LazyValue extends Value {
 	 * bug where TLC generates and incorrect set of states with certain statements.
 	 * More details can be found at https://github.com/tlaplus/tlaplus/issues/113.
 	 */
-	private static final boolean LAZYEVAL_OFF = Boolean.getBoolean(tlc2.value.impl.LazyValue.class.getName() + ".off");
+	public static final boolean LAZYEVAL_OFF = Boolean.getBoolean(tlc2.value.impl.LazyValue.class.getName() + ".off");
 	
 	static {
 		// Indicate if LazyValue will be disabled in this TLC run.
diff --git a/tlatools/org.lamport.tlatools/test-model/Github798I.tla b/tlatools/org.lamport.tlatools/test-model/Github798I.tla
new file mode 100644
index 0000000000000000000000000000000000000000..91cf9e095a5a0141aea4b8d053f21fc03e608669
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Github798I.tla
@@ -0,0 +1,31 @@
+---------------------------- MODULE Github798I ----------------------------
+S == {"n1", "n2"}
+
+Direct(xx, yy) ==
+    /\ xx \in [S -> {"a"}]
+    /\ yy \in [S -> S]
+    /\ \A s \in S : 
+        xx[s] = "a" => yy[s] = s
+
+Indirect(xx, yy) == 
+    /\ Direct(xx, yy)
+
+InIndirect(xx, yy) ==
+	LET zz == xx IN
+    Indirect(zz, yy)
+
+VARIABLE x, y
+
+vars == <<x, y>>
+
+Init ==
+    InIndirect(x, y)
+   
+Spec == 
+    Init /\ [][InIndirect(x', y')]_vars
+
+==========================================================================
+---------------------------- CONFIG Github798I -----------------------------
+SPECIFICATION
+    Spec
+===========================================================================
diff --git a/tlatools/org.lamport.tlatools/test-model/Github798N.tla b/tlatools/org.lamport.tlatools/test-model/Github798N.tla
new file mode 100644
index 0000000000000000000000000000000000000000..08171ccc799143aabeac22a0eb09eca0b6dbb636
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test-model/Github798N.tla
@@ -0,0 +1,35 @@
+---------------------------- MODULE Github798N ---------------------------
+S == {"n1", "n2"}
+
+Direct(xx, yy) ==
+    /\ xx \in [S -> {"a"}]
+    /\ yy \in [S -> S]
+    /\ \A s \in S : 
+        xx[s] = "a" => yy[s] = s
+
+Indirect(xx, yy) == 
+    /\ Direct(xx, yy)
+
+InIndirect(xx, yy) ==
+	LET zz == xx IN
+    Indirect(zz, yy)
+
+VARIABLE x, y
+
+vars == <<x, y>>
+
+Init == 
+	/\ x = {}
+	/\ y = {}
+
+Next ==
+    InIndirect(x', y')
+   
+Spec == 
+    Init /\ [][Next]_vars
+
+==========================================================================
+---------------------------- CONFIG Github798N ----------------------------
+SPECIFICATION
+    Spec
+===========================================================================
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java
new file mode 100644
index 0000000000000000000000000000000000000000..6dad1288fd45581996b2ffb0d18cdf2500080d7d
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java
@@ -0,0 +1,60 @@
+/*******************************************************************************
+ * Copyright (c) 2023 Microsoft Research. All rights reserved.
+ *
+ * The MIT License (MIT)
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.tool;
+
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import java.io.IOException;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class Github798ITest extends ModelCheckerTestCase {
+
+	public Github798ITest() {
+		super("Github798I", new String[] { "-config", "Github798I.tla" }, EC.ExitStatus.SUCCESS);
+	}
+
+	protected boolean noGenerateSpec() {
+		return true;
+	}
+
+	protected boolean doDumpTrace() {
+		return false;
+	}
+
+	@Test
+	public void testSpec() throws IOException {
+		assertTrue(recorder.recorded(EC.TLC_FINISHED));
+		assertFalse(recorder.recorded(EC.GENERAL));
+
+		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "2", "1", "0"));
+		assertTrue(recorder.recordedWithStringValue(EC.TLC_SEARCH_DEPTH, "1"));
+	}
+}
diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798NTest.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798NTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..2cb00946cc9329cd4975877b47ecd6bc3ecbd94b
--- /dev/null
+++ b/tlatools/org.lamport.tlatools/test/tlc2/tool/Github798NTest.java
@@ -0,0 +1,60 @@
+/*******************************************************************************
+ * Copyright (c) 2023 Microsoft Research. All rights reserved.
+ *
+ * The MIT License (MIT)
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ * of the Software, and to permit persons to whom the Software is furnished to do
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ *   Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.tool;
+
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
+
+import java.io.IOException;
+
+import org.junit.Test;
+
+import tlc2.output.EC;
+import tlc2.tool.liveness.ModelCheckerTestCase;
+
+public class Github798NTest extends ModelCheckerTestCase {
+
+	public Github798NTest() {
+		super("Github798N", new String[] { "-config", "Github798N.tla" }, EC.ExitStatus.SUCCESS);
+	}
+
+	protected boolean noGenerateSpec() {
+		return true;
+	}
+
+	protected boolean doDumpTrace() {
+		return false;
+	}
+
+	@Test
+	public void testSpec() throws IOException {
+		assertTrue(recorder.recorded(EC.TLC_FINISHED));
+		assertFalse(recorder.recorded(EC.GENERAL));
+
+		assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "3", "2", "0"));
+		assertTrue(recorder.recordedWithStringValue(EC.TLC_SEARCH_DEPTH, "2"));
+	}
+}
diff --git a/toolbox/org.lamport.tla.toolbox.doc/pom.xml b/toolbox/org.lamport.tla.toolbox.doc/pom.xml
index a559fc916941797f802a4ebdfaf2882a1b99465f..bccd675e87588daefb35a93e96f5cfaee1193420 100644
--- a/toolbox/org.lamport.tla.toolbox.doc/pom.xml
+++ b/toolbox/org.lamport.tla.toolbox.doc/pom.xml
@@ -11,7 +11,7 @@
   </parent>
   <groupId>tlatoolbox</groupId>
   <artifactId>org.lamport.tla.toolbox.doc</artifactId>
-  <version>1.7.1-SNAPSHOT</version>
+  <version>1.7.3-SNAPSHOT</version>
   <packaging>eclipse-plugin</packaging>
   <properties>
       <!-- Do not include non-code project in Sonar reporting. -->
diff --git a/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product b/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
index 2de5c6477f1556e023fdc4b61630d50b8fe020a5..0f6fdadfed6686db41c947731aff8df7564ab511 100644
--- a/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
+++ b/toolbox/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
@@ -1,16 +1,16 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <?pde version="3.5"?>
 
-<product name="TLA+ Toolbox" uid="org.lamport.tla.toolbox.product.product" id="org.lamport.tla.toolbox.product.standalone.product" application="org.lamport.tla.toolbox.application" version="1.7.2.qualifier" useFeatures="true" includeLaunchers="true">
+<product name="TLA+ Toolbox" uid="org.lamport.tla.toolbox.product.product" id="org.lamport.tla.toolbox.product.standalone.product" application="org.lamport.tla.toolbox.application" version="1.7.3.qualifier" useFeatures="true" includeLaunchers="true">
 
    <aboutInfo>
       <image path="/org.lamport.tla.toolbox.product.standalone/images/splash_small.png"/>
       <text>
          TLA+ Toolbox provides a user interface for TLA+ Tools. 
 
-This is Version 1.7.2 of 02 February 2022 and includes:
+This is Version 1.7.3 of 20 March 2023 and includes:
   - SANY Version 2.2 of 20 April 2020
-  - TLC Version 2.17 of 02 Febraury 2022
+  - TLC Version 2.18 of 20 March 2023
   - PlusCal Version 1.11 of 31 December 2020
   - TLATeX Version 1.0 of 20 September 2017
 
@@ -95,11 +95,11 @@ openFile
       <plugin id="org.lamport.tla.toolbox.jclouds" autoStart="true" startLevel="4" />
       <plugin id="packet" autoStart="true" startLevel="4" />
       <plugin id="sts" autoStart="true" startLevel="4" />
-      <property name="eclipse.buildId" value="1.7.2" />
+      <property name="eclipse.buildId" value="1.7.3" />
    </configurations>
 
    <repositories>
-      <repository location="http://lamport.org/tlatoolbox/branches/1.7.2/toolboxUpdate/" enabled="true" />
+      <repository location="http://lamport.org/tlatoolbox/branches/1.7.3/toolboxUpdate/" enabled="true" />
       <repository location="http://lamport.org/tlatoolbox/ci/toolboxUpdate/" enabled="false" />
    </repositories>
 
diff --git a/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml b/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml
index bd29e511149b9741082d1e20eb63b8d8ed0f79d4..6a78f6044bbb19bf8526050e90d2199985c15414 100644
--- a/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml
+++ b/toolbox/org.lamport.tla.toolbox.product.standalone/plugin.xml
@@ -30,7 +30,7 @@
          </property>
          <property
                name="aboutText"
-               value="TLA+ Toolbox provides a user interface for TLA+ Tools. &#x0A;&#x0A;This is Version 1.7.2 of 02 February 2022 and includes:&#x0A;  - SANY Version 2.2 of 20 April 2020&#x0A;  - TLC Version 2.17 of 02 February 2022&#x0A;  - PlusCal Version 1.11 of 31 December 2020&#x0A;  - TLATeX Version 1.0 of 20 September 2017&#x0A;&#x0A;Don&apos;t forget to click on help.  You can learn about features that you never knew about or have forgotten.&#x0A;&#x0A;Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .&#x0A;&#x0A;Some icons used in the Toolbox were provided by www.flaticon.com">
+               value="TLA+ Toolbox provides a user interface for TLA+ Tools. &#x0A;&#x0A;This is Version 1.7.3 of 20 March 2023 and includes:&#x0A;  - SANY Version 2.2 of 20 April 2020&#x0A;  - TLC Version 2.18 of 20 March 2023&#x0A;  - PlusCal Version 1.11 of 31 December 2020&#x0A;  - TLATeX Version 1.0 of 20 September 2017&#x0A;&#x0A;Don&apos;t forget to click on help.  You can learn about features that you never knew about or have forgotten.&#x0A;&#x0A;Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .&#x0A;&#x0A;Some icons used in the Toolbox were provided by www.flaticon.com">
          </property>
          <property
                name="aboutImage"
diff --git a/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java b/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
index d8c0d4ef620c2c070cfa440e6240e54b10a3e769..cd4544eca7500c12651c7fc509cd16ff82664df1 100644
--- a/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
+++ b/toolbox/org.lamport.tla.toolbox.product.standalone/src/org/lamport/tla/toolbox/ui/intro/ToolboxIntroPart.java
@@ -431,7 +431,7 @@ public class ToolboxIntroPart extends IntroPart implements IIntroPart {
 
 		final Label lblVersion = new Label(outerContainer, SWT.WRAP);
 		lblVersion.setLayoutData(new GridData(SWT.FILL, SWT.CENTER, false, false, 2, 1));
-		lblVersion.setText("Version 1.7.2 of 02 February 2022");
+		lblVersion.setText("Version 1.7.3 of 20 March 2023");
 		lblVersion.setBackground(backgroundColor);
 	}