From 3a5a8d7aded18ae1434b1392d00dd54306304a4d Mon Sep 17 00:00:00 2001 From: Boris Shingarov 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' }