diff --git a/src/SpriteLang/BlockClosure.extension.st b/src/SpriteLang/BlockClosure.extension.st
new file mode 100644
index 000000000..00163613f
--- /dev/null
+++ b/src/SpriteLang/BlockClosure.extension.st
@@ -0,0 +1,16 @@
+Extension { #name : #BlockClosure }
+
+{ #category : #'*SpriteLang' }
+BlockClosure >> runCG [
+"
+run :: CG a -> Either [UX.UserError] (a, CGInfo)
+run act = do
+  (x, s) <- runStateT act s0
+  return (x, cgInfo s)
+Cf. Constraints.hs
+"
+	| x s |
+	s := CGState s0.
+	x := self runReader: #cgi initialState: s.
+	^x -> s cgInfo
+]
diff --git a/src/SpriteLang/CGState.class.st b/src/SpriteLang/CGState.class.st
index 703e27178..0deffa172 100644
--- a/src/SpriteLang/CGState.class.st
+++ b/src/SpriteLang/CGState.class.st
@@ -17,25 +17,26 @@ Class {
 	#category : #'SpriteLang-CgMonad'
 }
 
-{ #category : #initialization }
+{ #category : #'state monad' }
 CGState class >> current [
-	current isNil ifTrue: [ current := self basicNew ].
-	^current
+	^Context readState: #cgi
 ]
 
-{ #category : #initialization }
+{ #category : #'instance creation' }
 CGState class >> new [
 	^self shouldNotImplement
 ]
 
-{ #category : #initialization }
-CGState class >> reset [ 
-	current := nil
+{ #category : #'instance creation' }
+CGState class >> s0 [
+	^self basicNew
+		count: 0;
+		cgInfo: CGInfo new;
+		yourself
 ]
 
 { #category : #accessing }
 CGState >> cgInfo [
-	cgInfo isNil ifTrue: [ cgInfo := CGInfo new ].
 	^ cgInfo
 ]
 
@@ -46,7 +47,6 @@ CGState >> cgInfo: anObject [
 
 { #category : #accessing }
 CGState >> count [
-	count isNil ifTrue: [ count := 0 ].
 	^ count
 ]
 
diff --git a/src/SpriteLang/Prog.class.st b/src/SpriteLang/Prog.class.st
index c26595058..169462aef 100644
--- a/src/SpriteLang/Prog.class.st
+++ b/src/SpriteLang/Prog.class.st
@@ -93,22 +93,21 @@ Prog >> solve [
 
 { #category : #verification }
 Prog >> vcgen [
-	| expr′ env expr′′ cstr query |
-
+	| expr′ env expr′′ c_cgi c cgi query |
 	expr′ := expr uniq2.
 	env := ΓContext empEnv: meas typs: data.
 	expr′′ := expr′ elaborate: env.
-	CGState reset.
-	cstr := expr′′ check: env rtype: TInt instance bTrue.
+	c_cgi := [ expr′′ check: env rtype: TInt instance bTrue ] runCG.
+	c := c_cgi key. cgi := c_cgi value.
 	query := HornQuery new.
-	cstr addToQuery: query.
-	CGInfo current cgiKVars do: [ :kVar | kVar addToQuery: query ].
+	c addToQuery: query.
+	cgi cgiKVars do: [ :kVar | kVar addToQuery: query ].
 	quals do: [ :q | q addToQuery: query ].
 	query qCon: (Dictionary newFromAssociations: meas).	
 	#(1 2 3) do: [ :j | query addPapp: j ].
-	CGInfo current cgiDefs   do: [ :equ  | equ  addToQuery: query ].
-	CGInfo current cgiConsts do: [ :con  | con  addToQuery: query ].
-	CGInfo current cgiDefs isEmpty ifFalse: [
+	cgi cgiDefs   do: [ :equ  | equ  addToQuery: query ].
+	cgi cgiConsts do: [ :con  | con  addToQuery: query ].
+	cgi cgiDefs isEmpty ifFalse: [
 		HOpt rewrite addToQuery: query
 	].
 	^query