From a4d453e50c816add3ecde44af11a0965c38c90b4 Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Thu, 21 Mar 2024 10:26:49 -0400
Subject: [PATCH] [PLE] Don't simplify Z3Nodes waiting for feedback on
https://github.com/Z3Prover/z3/issues/7179
---
src/PLE/Z3Node.extension.st | 2 +-
src/Z3/Z3Node.class.st | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/PLE/Z3Node.extension.st b/src/PLE/Z3Node.extension.st
index 235e32c66..8355a2b08 100644
--- a/src/PLE/Z3Node.extension.st
+++ b/src/PLE/Z3Node.extension.st
@@ -93,7 +93,7 @@ notGuardedApps :: Expr -> [Expr]
{ #category : #'*PLE' }
Z3Node >> simplify: γ in: ictx [
- ^[ :x | (x simplifyStep: γ in: ictx) simplify ] fix: self
+ ^[ :x | (x simplifyStep: γ in: ictx) "simplify" ] fix: self
]
{ #category : #'*PLE' }
diff --git a/src/Z3/Z3Node.class.st b/src/Z3/Z3Node.class.st
index 16c0e400e..bc1c4341a 100644
--- a/src/Z3/Z3Node.class.st
+++ b/src/Z3/Z3Node.class.st
@@ -200,7 +200,7 @@ Z3Node >> inEnvironment: aDictionary [
to add:(var coerce: val).
]
].
- ^(self substituteAll: from withoutNils with: to withoutNils) simplify
+ ^(self substituteAll: from withoutNils with: to withoutNils) "simplify"
]
{ #category : #'term rewriting' }