diff --git a/src/Refinements/Expr.class.st b/src/Refinements/Expr.class.st
index cd3ab11a9..1017e2bb1 100644
--- a/src/Refinements/Expr.class.st
+++ b/src/Refinements/Expr.class.st
@@ -109,7 +109,7 @@ Expr >> <=> rhs [
 { #category : #'theory symbols' }
 Expr >> === rhs [
 	^ECst
-		expr: (EMessageSend of: (MessageSend receiver: self selector: #=== argument: rhs))
+		expr: (PAtom brel: #=== x: self y: rhs)
 		sort: Bool sort
 ]
 
diff --git a/src/Refinements/PAtom.class.st b/src/Refinements/PAtom.class.st
index c18ecbbdb..139c68780 100644
--- a/src/Refinements/PAtom.class.st
+++ b/src/Refinements/PAtom.class.st
@@ -69,6 +69,19 @@ PAtom >> brel: anObject [
 	brel := anObject
 ]
 
+{ #category : #elaboration }
+PAtom >> elab: f [
+	| x′ y′ computed |
+	brel = Ueq ifTrue: [ self shouldBeImplemented ]. "| r == Ueq || r == Une = do…"
+	brel = Ueq ifTrue: [ self shouldBeImplemented ].
+	
+	"elab f@(env,_) (PAtom r e1 e2)"
+	x′ := (x elab: f) first.
+	y′ := (y elab: f) first.
+	computed := x′ perform: brel with: y′.
+	^{ computed . Bool sort }
+]
+
 { #category : #'term rewriting' }
 PAtom >> evaluateIn: aBindEnv ifUndeclared: vndBlock [
 	^(x evaluateIn: aBindEnv ifUndeclared: vndBlock)
@@ -97,6 +110,11 @@ PAtom >> printOn: aStream [
 	aStream nextPut: $).
 ]
 
+{ #category : #'SMT interface' }
+PAtom >> smt2 [
+	^x smt2 perform: brel with: y smt2
+]
+
 { #category : #'term rewriting' }
 PAtom >> subst1: θ [ 
 	^PAtom