diff --git a/.github/workflows/continuousIntegration.yml b/.github/workflows/continuousIntegration.yml
index 3ba0789f..29d60f62 100644
--- a/.github/workflows/continuousIntegration.yml
+++ b/.github/workflows/continuousIntegration.yml
@@ -64,6 +64,10 @@ jobs:
             test-dir: tests/smt
           - name: other
             test-dir: tests/error tests/froglet tests/srclocs tests/temporal
+          - name: custom-solver
+            test-dir: tests/forge/custom-solver
+            custom-run: true
+
     name: test-${{ matrix.name }}
     steps:
     - name: Checkout repo
@@ -106,7 +110,83 @@ jobs:
     - name: Run tests
       run: |
         cd forge/
-        chmod +x run-tests.sh
-        for dir in ${{ matrix.test-dir }}; do
-          ./run-tests.sh "$dir"
-        done
+        if [ "${{ matrix.custom-run }}" = "true" ]; then
+          cd ${{ matrix.test-dir }}
+          chmod +x run.sh subdir/run.sh
+          exitCode=0
+          for f in *.frg; do
+            echo "Running $f..."
+            if ! racket "$f" -O run_sterling 'off'; then
+              echo "FAILED: $f"
+              exitCode=1
+            fi
+          done
+          exit $exitCode
+        else
+          chmod +x run-tests.sh
+          for dir in ${{ matrix.test-dir }}; do
+            ./run-tests.sh "$dir"
+          done
+        fi
+
+  test-custom-solver-win:
+    needs: check-test-coverage
+    runs-on: windows-latest
+    name: test-custom-solver-win
+    steps:
+    - name: Checkout repo
+      uses: actions/checkout@v4
+
+    - name: Setup Racket
+      uses: Bogdanp/setup-racket@v1.14
+      with:
+        version: '8.15'
+
+    - name: Setup Java
+      uses: actions/setup-java@v4
+      with:
+        distribution: 'temurin'
+        java-version: '17'
+
+    - name: Cache Racket packages
+      uses: actions/cache@v4
+      with:
+        path: ~/AppData/Roaming/Racket
+        key: racket-pkgs-win-${{ hashFiles('forge/info.rkt') }}
+        restore-keys: racket-pkgs-win-
+
+    - name: Install Forge
+      run: |
+        raco pkg update --auto --no-docs --batch ./forge 2>$null; if ($LASTEXITCODE -ne 0) { raco pkg install --auto --no-docs ./forge }
+
+    - name: Run custom solver tests
+      shell: cmd
+      run: |
+        cd forge\tests\forge\custom-solver\win
+        set exitCode=0
+        for %%f in (*.frg) do (
+          echo Running %%f...
+          racket "%%f" -O run_sterling 'off'
+          if errorlevel 1 (
+            echo FAILED: %%f
+            set exitCode=1
+          )
+        )
+        exit /b %exitCode%
+
+    - name: Run custom solver tests (path with spaces)
+      shell: cmd
+      run: |
+        mkdir "forge\tests\forge\custom-solver\win space test"
+        xcopy /s /e /i "forge\tests\forge\custom-solver\win" "forge\tests\forge\custom-solver\win space test"
+        cd "forge\tests\forge\custom-solver\win space test"
+        set exitCode=0
+        for %%f in (*.frg) do (
+          echo Running %%f [space path]...
+          racket "%%f" -O run_sterling 'off'
+          if errorlevel 1 (
+            echo FAILED: %%f
+            set exitCode=1
+          )
+        )
+        exit /b %exitCode%
diff --git a/forge/domains/crypto/README.md b/forge/domains/crypto/README.md
index 1ae8fc5b..179044e9 100644
--- a/forge/domains/crypto/README.md
+++ b/forge/domains/crypto/README.md
@@ -84,6 +84,14 @@ Forge does _bounded_ model finding; that is, it renders the search problem decid
 
 E.g., we might say that there are no more than `3` names in an execution of the reflection protocol: the initiator's name, the responder's name, and the attacker's name. (The attacker must be present, as the model follows Dolev-Yao is making them the medium by which principles communicate.)
 
+#### Time
+
+The model has two different notions of time:
+  - The `Timeslot` sig, which represents the handling of a single message. This should always be either sent or received by the `Attacker`, who is synonymous with the medium of communication.
+  - The `Microtick` sig, which is used to properly order how agents learn values within nested encrypted terms. The scope for `Microtick` should never be lower than `2`, representing the pre-state where nothing has yet been learned and the post-state where a single layer of encryption has been removed. If a protocol requires deeper nesting, increment the scope on `Microtick` to one more than the nesting depth.
+
+Note that the `Microtick` sig was not present in the original paper, which used the `Timeslot` sig for both kinds of "time", resulting in poor performance.
+
 ### Visualizing Executions 
 
 When Sterling opens, the solver will (perhaps after some delay) produce an instance. The default visualization will appear as a dense cluster of boxes and lines. To switch to the sequence diagram version, click on the 'Script' tab and paste in the contents of the [visualization script](./vis/crypto_viz.js). Then click 'Run'. 
diff --git a/forge/domains/crypto/base.frg b/forge/domains/crypto/base.frg
index 0258140e..54937051 100644
--- a/forge/domains/crypto/base.frg
+++ b/forge/domains/crypto/base.frg
@@ -20,6 +20,12 @@
       as the protocol role execution.
     - This model embraces Dolev-Yao in a very concrete way: there is an explicit 
       attacker, who is also the medium of communication between participants.
+
+  Fall 2025 update:
+    - This model had previously used the `Timeslot` sig for both states between 
+      messages _and_ microticks (which allow "learning" within nested encrypted terms).
+      Instead, the model now uses a subset of the available time slots according to 
+      the user-provided scope on the `Microtick` sig.
 */
 
 -- NOTE WELL: `mesg` is what CPSA calls terms; we echo that here, do not confuse 
@@ -36,6 +42,7 @@ sig PublicKey extends akey {}
 one sig KeyPairs {
   pairs: set PrivateKey -> PublicKey,
   owners: func PrivateKey -> name,
+  -- There may be LTKs that aren't pre-assigned to a pair of agents. E.g., session keys.
   ltks: set name -> name -> skey
 }
 
@@ -54,8 +61,9 @@ fun getInv[k: Key]: one Key {
 }
 
 
--- Time indexes (t=0, t=1, ...). These are also used as micro-tick indexes, so the 
--- bound on `Timeslot` will also affect how many microticks are available between ticks.
+/** Time indexes corresponding to one message being sent and received.
+    Dropped messages are modeled as the medium receiving the message but 
+    not forwarding it. */
 sig Timeslot {
   -- structure of time (must be rendered linear in every run via `next is linear`)
   next: lone Timeslot,
@@ -67,7 +75,16 @@ sig Timeslot {
 
   -- relation is: Tick x Microtick x learned-mesg
   -- Only one agent per tick is receiving, so always know which agent's workspace it is
-  workspace: set Timeslot -> mesg
+  workspace: set Microtick -> mesg
+}
+
+/** A Microtick represents a step of _learning_ that is part of processing a single 
+    message reception. */
+sig Microtick {
+  -- structure of microticks. (must be rendered linear in every run via `next is linear`)
+  -- The `wellformed` predicate below contains constraints that enforce this, in case 
+  -- a user forgets the add the linear annotation, but doing so would harm performance. 
+  mt_next: lone Microtick
 }
 
 -- As names process received messages, they learn pieces of data
@@ -89,7 +106,7 @@ one sig Attacker extends name {}
 sig Ciphertext extends mesg {
    -- encrypted with this key
    encryptionKey: one Key,
-   -- result in concating plaintexts
+   -- concatenated plaintexts (order not currently modeled)
    plaintext: set mesg
 }
 
@@ -111,11 +128,29 @@ fun baseKnown[a: name]: set mesg {
     a
 }
 
+/** Time and micro-time are ordered. 
+    (This constraint should be tautologous if the user has given an `is linear` 
+    for `next` and `mt_next`.) */
+pred timeSafety {
+  some firstTimeslot: Timeslot | {
+    all ts: Timeslot | ts in firstTimeslot.*next
+    no firstTimeslot.~next
+    -- field declaration ensures at most one successor
+  }
+  some firstMicro: Microtick | {
+    all ts: Microtick  | ts in firstMicro.*mt_next
+    no firstMicro.~mt_next
+    -- field declaration ensures at most one successor
+  }
+}
+
 /** This (large) predicate contains the vast majority of domain axioms */
 pred wellformed {
   -- Design choice: only one message event per timeslot;
   --   assume we have a shared notion of time
-    
+
+  timeSafety
+
   -- You cannot send a message with no data
   all m: Timeslot | some m.data
 
@@ -124,10 +159,10 @@ pred wellformed {
 
   -- workspace: workaround to avoid cyclic justification within just deconstructions
   -- AGENT -> TICK -> MICRO-TICK LEARNED_SUBTERM
-  all d: mesg | all t, microt: Timeslot | let a = t.receiver.agent | d in (workspace[t])[microt] iff {
+  all d: mesg | all t: Timeslot, microt: Microtick | let a = t.receiver.agent | d in (workspace[t])[microt] iff {
     -- Base case:
-    -- received the data in the clear just now 
-    {d in t.data and no microt.~next}
+    -- received the data in the clear just now (first microtick)
+    {d in t.data and no microt.~mt_next}
     or
     -- Inductive case:
     -- breaking down a ciphertext we learned *previously*, or that we've produced from 
@@ -139,11 +174,20 @@ pred wellformed {
     { 
       --d not in ((a.workspace)[t])[Timeslot - microt.^next] and -- first time appearing
       {some superterm : Ciphertext | {      
-      d in superterm.plaintext and     
-      superterm in (a.learned_times).(Timeslot - t.*next) + workspace[t][Timeslot - microt.*next] + baseKnown[a] and
-      getInv[superterm.encryptionKey] in (a.learned_times).(Timeslot - t.*next) + workspace[t][Timeslot - microt.*next] + baseKnown[a]
+           -- the term in question is contained within superterm
+           d in superterm.plaintext 
+           and     
+           -- we had learned the superterm in a previous timeslot or previous microtick in this timeslot
+           superterm in (a.learned_times).(Timeslot - t.*next) + 
+                        workspace[t][Microtick - microt.*mt_next] + 
+                        baseKnown[a] 
+           and
+           -- we had also learned how to decrypt the superterm previously
+           getInv[superterm.encryptionKey] in (a.learned_times).(Timeslot - t.*next) + 
+                                              workspace[t][Microtick - microt.*mt_next] + 
+                                              baseKnown[a]
     }}}
-  }
+  } -- end block for workspace 
  
   -- names only learn information that associated strands are explicitly sent 
   -- (start big disjunction for learned_times)
@@ -166,7 +210,7 @@ pred wellformed {
     -- consider: (k1, enc(k2, enc(n1, invk(k2)), invk(k1)))
     -- or, worse: (k1, enc(x, invk(k3)), enc(k2, enc(k3, invk(k2)), invk(k1)))
     { t.receiver.agent = a
-      d in workspace[t][Timeslot] -- derived in any micro-tick in this (reception) timeslot
+      d in workspace[t][Microtick] -- derived in any micro-tick in this (reception) timeslot
     }   
     or 
     -- construct encrypted terms (only allow at NON-reception time; see above)
@@ -190,7 +234,8 @@ pred wellformed {
 
   -- Messages comprise only values known by the sender
   all m: Timeslot | m.data in (((m.sender).agent).learned_times).(Timeslot - m.^next) 
-  -- Always send or receive to the adversary
+
+  -- Always send or receive to the adversary (who is the "medium of communication")
   all m: Timeslot | m.sender = AttackerStrand or m.receiver = AttackerStrand 
 
   -- plaintext relation is acyclic  
diff --git a/forge/domains/crypto/examples/blanchet-corrected.frg b/forge/domains/crypto/examples/blanchet-corrected.frg
new file mode 100644
index 00000000..6ce71f0f
--- /dev/null
+++ b/forge/domains/crypto/examples/blanchet-corrected.frg
@@ -0,0 +1,122 @@
+#lang forge
+
+// Protocol definitions in CPSA DSL
+open "blanchet-corrected.rkt" 
+// Domain-specific visualizer script
+option run_sterling "../vis/crypto_viz.js"
+
+pred blanchet_corrected_run {
+    exec_blanchet_corrected_init
+    exec_blanchet_corrected_resp
+    
+    -- Do not run more than one skeleton at a time.
+    -- constrain_skeleton_blanchet_0  -- init strand perspective 
+    -- constrain_skeleton_blanchet_1  -- sat by self
+
+    -- This contains a "listener strand", which the expander turns into 
+    -- #`(in (join #,this-strand-or-skeleton #,(id-converter pname strand-role-or-skeleton-idx v))
+    --           (join Attacker learned_times Timeslot)))
+    -- That is: the attacker learns the value of this strand variable at some point in time.
+    --  (It does NOT create a separate listener strand, it just checks the attacker's knowledge base.)
+    constrain_skeleton_blanchet_corrected_2 -- responder strand perspective (with 1 commented out skeleton)
+    
+    wellformed
+}
+
+/** The attacker has no long-term keys. */
+pred atk_no_ltks {
+   // KeyPairs.ltks:  set name -> name -> skey
+
+    no Attacker.(KeyPairs.ltks)
+    // Simplified from:
+    //(no (+ (join Attacker (join name     (join KeyPairs ltks)))
+    //       (join name     (join Attacker (join KeyPairs ltks)))))
+}
+
+
+// Bounds can be quite troublesome. Count carefully.
+run {
+    blanchet_corrected_run
+    atk_no_ltks
+
+    // The attacker is not playing a game by themselves
+    // It's unclear if this should just be a base assumption. But we do want the attacker to
+    // be able to own multiple strands. 
+    blanchet_corrected_init.agent != Attacker
+    blanchet_corrected_resp.agent != Attacker
+
+    // The keys used by the initiator are of the proper types. The CPSA definition just says they are 
+    // asymmetric keys, not that (e.g.) the outermost encryption key was a public key.
+    blanchet_corrected_init.blanchet_corrected_init_a in PublicKey
+    blanchet_corrected_init.blanchet_corrected_init_b in PublicKey
+
+    // The symmetric key sent is not pre-assigned to any agent pair. 
+    no KeyPairs.ltks.(blanchet_corrected_init.blanchet_corrected_init_s)
+
+
+} for exactly 1 KeyPairs, exactly 4 Timeslot,  20 mesg, 9 Key, 6 akey, 3 PrivateKey, 3 PublicKey, 
+              3 skey, 3 name, 1 Attacker, 3 text, exactly 5 Ciphertext, exactly 1 AttackerStrand, 
+              exactly 1 blanchet_corrected_init, exactly 1 blanchet_corrected_resp, exactly 3 strand, 
+              //exactly 1 skeleton_blanchet_0, 
+              //exactly 1 skeleton_blanchet_1, 
+              exactly 1 skeleton_blanchet_corrected_2
+              
+              , 5 Int
+              
+              , 3 Microtick
+
+  for {next is linear
+       mt_next is linear}
+
+    //   #:scope [(KeyPairs 1 1)
+    //            (Timeslot 4 4) 
+    //            (Message 4 4)
+               
+    //            (mesg 20) ; 9 + 3 + 3 + 5
+               
+    //            (Key 9)
+    //            (akey 6)               
+    //            (PrivateKey 3)
+    //            (PublicKey 3)
+    //            (skey 3)
+               
+    //            (name 3)
+    //            (Attacker 1 1)
+               
+    //            (text 3) ; includes data
+               
+    //            (Ciphertext 5 5)               
+               
+    //            (AttackerStrand 1 1)               
+    //            (blanchet_init 1 1)
+    //            (blanchet_resp 1 1)               
+    //            (strand 3 3)
+               
+    //            (skeleton_blanchet_0 1 1)
+    //            (skeleton_blanchet_1 1 1)
+    //            (skeleton_blanchet_2 1 1)               
+    //            (Int 5)
+    //            ]
+    //   ;#:expect sat
+    //   )
+
+
+
+/*
+
+(defprotocol blanchet basic             OS-EPL term count, if all distinct (recall inv denotes counterpart keys)
+  (defrole init                         ------------------------
+    (vars (a b akey) (s skey) (d data)) + 4 akey, 1 skey, 1 data
+    (trace
+     (send (enc (enc s (invk a)) b))    + 2 ciphertext
+     (recv (enc d s)))                  + 1 ciphertext
+    (uniq-orig s))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data)) + 4 akey, 1 skey, 1 data
+    (trace
+     (recv (enc (enc s (invk a)) b))    + 2 ciphertext
+     (send (enc d s)))                  + 1 ciphertext
+    (uniq-orig d))                      ------------------------
+  (comment "Blanchet's protocol"))        8 akey, 2 skey, 2 data, 6 ciphertext
+
+*/
\ No newline at end of file
diff --git a/forge/domains/crypto/examples/blanchet-corrected.rkt b/forge/domains/crypto/examples/blanchet-corrected.rkt
new file mode 100644
index 00000000..b1981bde
--- /dev/null
+++ b/forge/domains/crypto/examples/blanchet-corrected.rkt
@@ -0,0 +1,116 @@
+#lang forge/domains/crypto
+
+; If 
+;  (1) the init strand and the resp strand can share a knowledge base
+;    due to running on the same agent, and 
+;  (2) the attacker can generate d at the start, then
+;  Attacker ----> resp
+;  Attacker <---- resp
+;   [now resp knows the value, and so does init]
+;  init ----> Attacker [using same value]
+;  init <---- Attacker
+;   - d is uniquely originating (with Attacker)
+;   - the attacker knows d (they generated it!)
+;
+
+; Wait: is that value of d uniquely originated?
+; Possibly underconstrained origination predicate??
+
+;               (no (join Attacker generated_times 
+;                 (join blanchet-corrected_resp blanchet-corrected_resp_d)))
+
+
+;  so we require that Attacker did not generate (responder's) d value
+
+(defprotocol blanchet_corrected basic
+  (defrole init
+    (vars (a b akey) (s skey) (d data))
+    (trace
+     (send (enc (enc s b (invk a)) b))
+     (recv (enc d s)))
+    (uniq-orig s))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data))
+    (trace
+     (recv (enc (enc s b (invk a)) b))
+     (send (enc d s)))
+    (uniq-orig d))
+  (comment "Corrected Blanchet's protocol"))
+
+(defskeleton blanchet_corrected
+  (vars (a b akey) (s skey) (d data))
+  (defstrand init 2 (a a) (b b) (s s) (d d))
+  (non-orig (invk b))
+  (comment "Analyze from the initiator's perspective"))
+
+(defskeleton blanchet_corrected
+  (vars (a b akey) (s skey) (d data))
+  (defstrand init 2 (a a) (b b) (s s) (d d))
+  (deflistener d)
+  (non-orig (invk b))
+  (comment "From the initiator's perspective, is the secret leaked?"))
+
+; The scenario the manual describes shows the *responder*'s value
+; being compromised, but not the initiator's. Right now, our model
+; will create a constraint for both listeners (conjuctively), yielding
+; a spurious unsat result unless the initiator's deflistener is removed.
+;(defskeleton blanchet-corrected
+;  (vars (a b akey) (s skey) (d data))
+;  (defstrand resp 2 (a a) (b b) (s s) (d d))
+;  (non-orig (invk a) (invk b))
+;  (comment "Analyze from the responder's perspective"))
+
+(defskeleton blanchet_corrected
+  (vars (a b akey) (s skey) (d data))
+  (defstrand resp 2 (a a) (b b) (s s) (d d))
+  (deflistener d)
+  (non-orig (invk a) (invk b))
+  (comment "From the responders's perspective, is the secret leaked?"))
+
+; (run blanchet_corrected
+;       #:preds [
+;                exec_blanchet-corrected_init
+;                exec_blanchet-corrected_resp
+;               ; constrain_skeleton_blanchet-corrected_0
+;               ; constrain_skeleton_blanchet-corrected_1
+;                constrain_skeleton_blanchet-corrected_2 ; note this is the fourth skeleton including commented-out               
+;                wellformed
+
+;                ; The attacker has no long-term keys
+;                (no (+ (join Attacker (join name (join KeyPairs ltks)))
+;                       (join name (join Attacker (join KeyPairs ltks)))))
+;                ]
+;       #:bounds [(is next linear)]
+;       #:scope [(KeyPairs 1 1)
+;                (Timeslot 4 4) 
+;               ; (Message 4 4)
+               
+;                (mesg 20) ; 9 + 3 + 3 + 5
+               
+;                (Key 9)
+;                (akey 6)               
+;                (PrivateKey 3)
+;                (PublicKey 3)
+;                (skey 3)
+               
+;                (name 3)
+;                (Attacker 1 1)
+               
+;                (text 3) ; includes data
+               
+;                (Ciphertext 5 5)               
+               
+;                (AttackerStrand 1 1)               
+;                (blanchet-corrected_init 1 1)
+;                (blanchet-corrected_resp 1 1)               
+;                (strand 3 3)
+               
+;                (skeleton_blanchet-corrected_0 1 1)
+;                (skeleton_blanchet-corrected_1 1 1)
+;                (skeleton_blanchet-corrected_2 1 1)               
+;                (Int 5)
+;                ]
+;       ;#:expect sat
+;       )
+
+; (display blanchet_corrected)
\ No newline at end of file
diff --git a/forge/domains/crypto/examples/blanchet.frg b/forge/domains/crypto/examples/blanchet.frg
new file mode 100644
index 00000000..932a0cd0
--- /dev/null
+++ b/forge/domains/crypto/examples/blanchet.frg
@@ -0,0 +1,170 @@
+#lang forge
+
+// Protocol definitions in CPSA DSL
+open "blanchet.rkt" 
+// Domain-specific visualizer script
+option run_sterling "../vis/crypto_viz.js"
+
+/*
+  Note: the CPSA definition here says only that the initiator is encrypting their message
+        with *an asymmetric key*. If they encrypt with a _private_ key then of course the 
+        attacker can immediately read their message.
+  The CPSA manual says that `akey` is the sort of asymmetric keys, so (inv k) doesn't 
+  only operate on public keys.
+
+  ---------------------------------------------------------------------------------------
+
+  https://bblanche.gitlabpages.inria.fr/publications/BlanchetETAPS12.pdf
+
+  In the paper, it is an encrypted term, wrapping a signed term containing a symmetric key.
+
+        """
+        Message 1. A → B : {{k}skA}pkB     k fresh
+        Message 2. B → A : {s}k
+
+        In general, in the literature, as in the example above, the protocols are de-
+        scribed informally by giving the list of messages that should be exchanged be-
+        tween the principals. Nevertheless, one must be careful that these descriptions
+        are only informal: they indicate what happens in the absence of an adversary.
+        However, an adversary can capture messages and send his own messages, so the
+        source and the target of a message may not be the expected one. Moreover,
+        these descriptions leave implicit the verifications done by the principals when
+        they receive messages. Since the adversary may send messages different from
+        the expected ones, and exploit the obtained reply, these verifications are very
+        important: they determine which messages will be accepted or rejected, and
+        may therefore protect or not against attacks.
+
+        Although the explanation above may seem to justify its security informally,
+        this protocol is subject to an attack:
+
+        Message 1. A → C : {{k}skA}pkC
+        Message 1’. C(A) → B : {{k}skA}pkB
+        Message 2. B → C(A) : {s}k
+        """
+        
+    This attack is quite similar to the one against Needham-Schroeder in spirit, 
+    although the protocol has a very different shape.
+
+  * What logic exists in this model for verifying keys? 
+
+*/
+
+pred blanchet_run {
+    exec_blanchet_init
+    exec_blanchet_resp
+    
+    -- Do not run more than one skeleton at a time.
+    -- constrain_skeleton_blanchet_0  -- init strand perspective 
+    -- constrain_skeleton_blanchet_1  -- sat by self
+
+    -- This contains a "listener strand", which the expander turns into 
+    -- #`(in (join #,this-strand-or-skeleton #,(id-converter pname strand-role-or-skeleton-idx v))
+    --           (join Attacker learned_times Timeslot)))
+    -- That is: the attacker learns the value of this strand variable at some point in time.
+    --  (It does NOT create a separate listener strand, it just checks the attacker's knowledge base.)
+    constrain_skeleton_blanchet_2 -- responder strand perspective (with 1 commented out skeleton)
+    
+    // constrain_skeleton_blanchet_3 // note this is the fourth skeleton if including commented out
+    wellformed
+}
+
+/** The attacker has no long-term keys. */
+pred atk_no_ltks {
+   // KeyPairs.ltks:  set name -> name -> skey
+
+    no Attacker.(KeyPairs.ltks)
+    // Simplified from:
+    //(no (+ (join Attacker (join name     (join KeyPairs ltks)))
+    //       (join name     (join Attacker (join KeyPairs ltks)))))
+}
+
+
+// Bounds can be quite troublesome. Count carefully.
+run {
+    blanchet_run
+    atk_no_ltks
+
+    // The attacker is not playing a game by themselves
+    // It's unclear if this should just be a base assumption. But we do want the attacker to
+    // be able to own multiple strands. 
+    blanchet_init.agent != Attacker
+    blanchet_resp.agent != Attacker
+
+    // TODO DESIGN NOTE: I feel like some of these should be axiomatic, but aren't guaranteed by CPSA.
+    //  It's worth asking: are there CPSA constraints that I'm unaware of?
+
+    // The keys used by the initiator are of the proper types. The CPSA definition just says they are 
+    // asymmetric keys, not that (e.g.) the outermost encryption key was a public key.
+    blanchet_init.blanchet_init_a in PublicKey
+    blanchet_init.blanchet_init_b in PublicKey
+
+    // The symmetric key sent is not pre-assigned to any agent pair. 
+    no KeyPairs.ltks.(blanchet_init.blanchet_init_s)
+
+
+} for exactly 1 KeyPairs, exactly 4 Timeslot,  20 mesg, 9 Key, 6 akey, 3 PrivateKey, 3 PublicKey, 
+              3 skey, 3 name, 1 Attacker, 3 text, exactly 5 Ciphertext, exactly 1 AttackerStrand, 
+              exactly 1 blanchet_init, exactly 1 blanchet_resp, exactly 3 strand, 
+              //exactly 1 skeleton_blanchet_0, 
+              //exactly 1 skeleton_blanchet_1, 
+              exactly 1 skeleton_blanchet_2
+              
+              , 5 Int
+              
+              , 3 Microtick
+
+  for {next is linear
+       mt_next is linear}
+
+    //   #:scope [(KeyPairs 1 1)
+    //            (Timeslot 4 4) 
+    //            (Message 4 4)
+               
+    //            (mesg 20) ; 9 + 3 + 3 + 5
+               
+    //            (Key 9)
+    //            (akey 6)               
+    //            (PrivateKey 3)
+    //            (PublicKey 3)
+    //            (skey 3)
+               
+    //            (name 3)
+    //            (Attacker 1 1)
+               
+    //            (text 3) ; includes data
+               
+    //            (Ciphertext 5 5)               
+               
+    //            (AttackerStrand 1 1)               
+    //            (blanchet_init 1 1)
+    //            (blanchet_resp 1 1)               
+    //            (strand 3 3)
+               
+    //            (skeleton_blanchet_0 1 1)
+    //            (skeleton_blanchet_1 1 1)
+    //            (skeleton_blanchet_2 1 1)               
+    //            (Int 5)
+    //            ]
+    //   ;#:expect sat
+    //   )
+
+
+
+/*
+
+(defprotocol blanchet basic             OS-EPL term count, if all distinct (recall inv denotes counterpart keys)
+  (defrole init                         ------------------------
+    (vars (a b akey) (s skey) (d data)) + 4 akey, 1 skey, 1 data
+    (trace
+     (send (enc (enc s (invk a)) b))    + 2 ciphertext
+     (recv (enc d s)))                  + 1 ciphertext
+    (uniq-orig s))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data)) + 4 akey, 1 skey, 1 data
+    (trace
+     (recv (enc (enc s (invk a)) b))    + 2 ciphertext
+     (send (enc d s)))                  + 1 ciphertext
+    (uniq-orig d))                      ------------------------
+  (comment "Blanchet's protocol"))        8 akey, 2 skey, 2 data, 6 ciphertext
+
+*/
\ No newline at end of file
diff --git a/forge/domains/crypto/examples/blanchet.rkt b/forge/domains/crypto/examples/blanchet.rkt
new file mode 100644
index 00000000..da1829ca
--- /dev/null
+++ b/forge/domains/crypto/examples/blanchet.rkt
@@ -0,0 +1,54 @@
+#lang forge/domains/crypto
+
+; https://bblanche.gitlabpages.inria.fr/publications/BlanchetETAPS12.pdf
+
+;(herald "Blanchet's Simple Example Protocol"
+;  (comment "There is a flaw in this protocol by design"))
+
+(defprotocol blanchet basic
+  (defrole init
+    (vars (a b akey) (s skey) (d data))
+    (trace
+     (send (enc (enc s (invk a)) b))
+     (recv (enc d s)))
+    (uniq-orig s))
+  (defrole resp
+    (vars (a b akey) (s skey) (d data))
+    (trace
+     (recv (enc (enc s (invk a)) b))
+     (send (enc d s)))
+    (uniq-orig d))
+  (comment "Blanchet's protocol"))
+
+; Skeleton 0
+(defskeleton blanchet
+  (vars (a b akey) (s skey) (d data))
+  (defstrand init 2 (a a) (b b) (s s) (d d))
+  (non-orig (invk b))
+  (comment "Analyze from the initiator's perspective"))
+
+; Skeleton 1
+(defskeleton blanchet
+  (vars (a b akey) (s skey) (d data))
+  (defstrand resp 2 (a a) (b b) (s s) (d d))
+  (non-orig (invk a) (invk b))
+  (comment "Analyze from the responder's perspective"))
+
+; The scenario the manual describes shows the *responder*'s value
+; being compromised, but not the initiator's. Right now, our model
+; will create a constraint for both listeners (conjuctively), yielding
+; a spurious unsat result unless the initiator's deflistener is removed.
+;(defskeleton blanchet
+;  (vars (a b akey) (s skey) (d data))
+;  (defstrand init 2 (a a) (b b) (s s) (d d))
+;  (deflistener d)
+;  (non-orig (invk b))
+;  (comment "From the initiator's perspective, is the secret leaked?"))
+
+; Skeleton 2 (assuming the above skeleton is commented out)
+(defskeleton blanchet
+  (vars (a b akey) (s skey) (d data))
+  (defstrand resp 2 (a a) (b b) (s s) (d d))
+  (deflistener d)
+  (non-orig (invk a) (invk b))
+  (comment "From the responders's perspective, is the secret leaked?"))
\ No newline at end of file
diff --git a/forge/domains/crypto/examples/ns.frg b/forge/domains/crypto/examples/ns.frg
index 19087f61..532a8ab2 100644
--- a/forge/domains/crypto/examples/ns.frg
+++ b/forge/domains/crypto/examples/ns.frg
@@ -50,6 +50,12 @@ pred attack_conditions {
   ns_resp.agent != Attacker
 }
 
+// Uncomment these only for debugging purposes.
+// option solver MiniSatProver
+// option logtranslation 2
+// option coregranularity 2
+// option core_minimization rce
+
 ns_attack_witness: run {
     wellformed // wellformedness assumptions from domain model
     attack_conditions // various conditions for the attack
@@ -60,9 +66,11 @@ ns_attack_witness: run {
     
     attack_exists // find a trace witnessing the attack
     
-  } for exactly 6 Timeslot, exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
+  } for exactly 6 Timeslot, exactly 2 Microtick,
+    exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
     exactly 2 text, exactly 5 Ciphertext, exactly 1 ns_init, exactly 1 ns_resp,
     exactly 3 PublicKey, exactly 3 PrivateKey, 0 skey, exactly 6 akey, exactly 3 strand,
     6 Int 
     // TODO change over to some-based bounds
-    for {next is linear} 
+    for {next is linear 
+        mt_next is linear}  
diff --git a/forge/domains/crypto/examples/ns_fixed.frg b/forge/domains/crypto/examples/ns_fixed.frg
index 99a3a5f8..d5d5520e 100644
--- a/forge/domains/crypto/examples/ns_fixed.frg
+++ b/forge/domains/crypto/examples/ns_fixed.frg
@@ -63,9 +63,12 @@ ns_fixed_attack_unsat: run {
     
     attack_exists // find a trace witnessing the attack
     
-  } for exactly 6 Timeslot, exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
+  } for exactly 6 Timeslot, exactly 2 Microtick,
+    exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
     exactly 2 text, exactly 5 Ciphertext, exactly 1 ns_init, exactly 1 ns_resp,
     exactly 3 PublicKey, exactly 3 PrivateKey, 0 skey, exactly 6 akey, exactly 3 strand,
     6 Int 
     // TODO change over to some-based bounds
-    for {next is linear} 
+    for {next is linear 
+        mt_next is linear} 
+
diff --git a/forge/domains/crypto/examples/reflect.frg b/forge/domains/crypto/examples/reflect.frg
index 978b7847..771727eb 100644
--- a/forge/domains/crypto/examples/reflect.frg
+++ b/forge/domains/crypto/examples/reflect.frg
@@ -42,7 +42,7 @@ reflect_responder_pov: run {
       //     uses the Attacker as the medium of communication. 
       //   - we follow CPSA terminology and use `mesg` to refer to any term, including plaintexts.
       //     Hence the high bound on `mesg`. 
-      exactly 4 Timeslot, 13 mesg,  
+      exactly 4 Timeslot, exactly 2 Microtick, 13 mesg,  
       // How many keys, and of what type, can exist in an execution of the protocol?
       exactly 1 KeyPairs, exactly 6 Key, exactly 6 akey, 0 skey, 
       exactly 3 PrivateKey, exactly 3 PublicKey,
@@ -54,7 +54,9 @@ reflect_responder_pov: run {
       1 Int
   // Manufacture bounds so that Timeslots are in linear ordering 
   // (similar to Alloy's ordering module: `open util/ordering[Timeslot]`)
-  for {next is linear}
+    for {next is linear 
+        mt_next is linear} 
+
 
 /*
   Note on bounds:
diff --git a/forge/domains/crypto/examples/tests/blanchet.test.frg b/forge/domains/crypto/examples/tests/blanchet.test.frg
new file mode 100644
index 00000000..400afd7a
--- /dev/null
+++ b/forge/domains/crypto/examples/tests/blanchet.test.frg
@@ -0,0 +1,31 @@
+#lang forge 
+
+open "../../base.frg"
+open "../blanchet.rkt"
+open "../blanchet.frg"
+option run_sterling off
+
+TEST_blanchet_attack_witness: assert {
+    blanchet_run
+    atk_no_ltks
+    blanchet_init.agent != Attacker
+    blanchet_resp.agent != Attacker
+    blanchet_init.blanchet_init_a in PublicKey
+    blanchet_init.blanchet_init_b in PublicKey
+    no KeyPairs.ltks.(blanchet_init.blanchet_init_s)
+} is sat for exactly 1 KeyPairs, exactly 4 Timeslot, 20 mesg, 
+              // NOTE WELL: not giving "exactly" here causes unnecessary bounds increase.
+              // TODO: investigate and refactor
+              exactly 9 Key, exactly 6 akey, exactly 3 PrivateKey, exactly 3 PublicKey, exactly 3 skey, 
+              3 name, 1 Attacker, 3 text, exactly 5 Ciphertext, exactly 1 AttackerStrand, 
+              exactly 1 blanchet_init, exactly 1 blanchet_resp, exactly 3 strand, 
+              // Must have the skeletons present, even if they are unused 
+              exactly 1 skeleton_blanchet_0, 
+              exactly 1 skeleton_blanchet_1, 
+              exactly 1 skeleton_blanchet_2
+              
+              //, 5 Int
+              
+              , 3 Microtick
+  for {next is linear
+       mt_next is linear}
\ No newline at end of file
diff --git a/forge/domains/crypto/examples/tests/ns.test.frg b/forge/domains/crypto/examples/tests/ns.test.frg
new file mode 100644
index 00000000..fc6e73f7
--- /dev/null
+++ b/forge/domains/crypto/examples/tests/ns.test.frg
@@ -0,0 +1,24 @@
+#lang forge 
+
+open "../../base.frg"
+open "../ns.rkt"
+open "../ns.frg"
+option run_sterling "../../vis/crypto_viz.js"
+
+TEST_ns_attack_witness: assert {
+    wellformed // wellformedness assumptions from domain model
+    attack_conditions // various conditions for the attack
+    success // the execution "succeeds" (initiator and responder learn secrets)
+    exec_ns_init // this is an execution for the initiator
+    exec_ns_resp // this is an execution for the responder
+    constrain_skeleton_ns_1 // take responder POV, where CPSA shows the attack behavior                                
+    
+    attack_exists // find a trace witnessing the attack
+    
+  } is sat for 
+    exactly 6 Timeslot, exactly 2 Microtick,
+    exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
+    exactly 2 text, exactly 5 Ciphertext, exactly 1 ns_init, exactly 1 ns_resp,
+    exactly 3 PublicKey, exactly 3 PrivateKey, 0 skey, exactly 6 akey, exactly 3 strand,
+    6 Int 
+    for {next is linear  mt_next is linear} 
\ No newline at end of file
diff --git a/forge/domains/crypto/examples/tests/ns_fixed.test.frg b/forge/domains/crypto/examples/tests/ns_fixed.test.frg
new file mode 100644
index 00000000..a442be01
--- /dev/null
+++ b/forge/domains/crypto/examples/tests/ns_fixed.test.frg
@@ -0,0 +1,24 @@
+#lang forge 
+
+open "../../base.frg"
+open "../ns_fixed.rkt"
+open "../ns_fixed.frg"
+option run_sterling "../../vis/crypto_viz.js"
+
+TEST_ns_fixed_attack_unsat: assert {
+    wellformed // wellformedness assumptions from domain model
+    attack_conditions // various conditions for the attack
+    success // the execution "succeeds" (initiator and responder learn secrets)
+    exec_ns_init // this is an execution for the initiator
+    exec_ns_resp // this is an execution for the responder
+    constrain_skeleton_ns_1 // take responder POV, where CPSA shows the attack behavior                                
+    
+    attack_exists // find a trace witnessing the attack
+    
+  } is unsat for 
+    exactly 6 Timeslot, exactly 2 Microtick,
+    exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
+    exactly 2 text, exactly 5 Ciphertext, exactly 1 ns_init, exactly 1 ns_resp,
+    exactly 3 PublicKey, exactly 3 PrivateKey, 0 skey, exactly 6 akey, exactly 3 strand,
+    6 Int 
+    for {next is linear  mt_next is linear} 
\ No newline at end of file
diff --git a/forge/domains/crypto/examples/tests/reflect.test.frg b/forge/domains/crypto/examples/tests/reflect.test.frg
new file mode 100644
index 00000000..3b20e64c
--- /dev/null
+++ b/forge/domains/crypto/examples/tests/reflect.test.frg
@@ -0,0 +1,25 @@
+#lang forge 
+
+open "../../base.frg"
+open "../reflect.rkt"
+open "../reflect.frg"
+option run_sterling "../../vis/crypto_viz.js"
+
+// See reflect.frg for documentation.
+TEST_reflect_responder_pov: assert {
+  wellformed                   
+  exec_reflect_init           
+  exec_reflect_resp            
+  constrain_skeleton_reflect_2 
+  reflect_resp.agent != reflect_init.agent
+  reflect_resp.reflect_resp_a != getInv[reflect_resp.reflect_resp_b]    
+  reflect_resp.reflect_resp_b != getInv[reflect_resp.reflect_resp_a]
+} is sat for 
+      exactly 4 Timeslot, exactly 2 Microtick, 13 mesg,  
+      exactly 1 KeyPairs, exactly 6 Key, exactly 6 akey, 0 skey, 
+      exactly 3 PrivateKey, exactly 3 PublicKey,
+      exactly 3 name, 0 text, exactly 4 Ciphertext,
+      exactly 1 reflect_init, exactly 1 reflect_resp,
+      1 Int
+    for {next is linear 
+        mt_next is linear} 
diff --git a/forge/domains/crypto/vis/crypto_viz.js b/forge/domains/crypto/vis/crypto_viz.js
index a1f51134..bbf8f505 100644
--- a/forge/domains/crypto/vis/crypto_viz.js
+++ b/forge/domains/crypto/vis/crypto_viz.js
@@ -5,7 +5,7 @@ const d3 = require('d3')
 // if you manually set this to something bigger than 100%, however.
 const svgContainer = document.getElementById('svg-container')
 svgContainer.getElementsByTagName('svg')[0].style.height = '100%'
-svgContainer.getElementsByTagName('svg')[0].style.width = '100%'
+svgContainer.getElementsByTagName('svg')[0].style.width = '200%'
 
 // constants for our visualization
 const BASE_X = 150;
diff --git a/forge/pardinus-cli/server/kks.rkt b/forge/pardinus-cli/server/kks.rkt
index c77c0201..10cccf7e 100755
--- a/forge/pardinus-cli/server/kks.rkt
+++ b/forge/pardinus-cli/server/kks.rkt
@@ -250,7 +250,7 @@
      (read-ack port err-port)]
     [(list (== 'ack) id)     
      id]    
-    [(== eof)     
+    [(== eof)
      (error (format "~a CLI shut down unexpectedly while sending problem definition!" server-name))]
     [else
      (port-echo err-port (current-error-port) #:title server-name)
diff --git a/forge/tests/forge/custom-solver/custom_solver.frg b/forge/tests/forge/custom-solver/custom_solver.frg
new file mode 100644
index 00000000..deddc1c7
--- /dev/null
+++ b/forge/tests/forge/custom-solver/custom_solver.frg
@@ -0,0 +1,9 @@
+#lang forge
+option solver "./run.sh"
+option run_sterling off
+
+sig Node {edges: set Node}
+
+test expect {
+    s: {some edges} for 1 Node is sat
+}
diff --git a/forge/tests/forge/custom-solver/custom_solver_froglet.frg b/forge/tests/forge/custom-solver/custom_solver_froglet.frg
new file mode 100644
index 00000000..ba08b4f5
--- /dev/null
+++ b/forge/tests/forge/custom-solver/custom_solver_froglet.frg
@@ -0,0 +1,9 @@
+#lang forge/froglet
+option solver "./run.sh"
+option run_sterling off
+
+sig Node {edges: lone Node}
+
+test expect {
+    s: {some n: Node | some n.edges} for 1 Node is sat
+}
diff --git a/forge/tests/forge/custom-solver/custom_solver_subdir.frg b/forge/tests/forge/custom-solver/custom_solver_subdir.frg
new file mode 100644
index 00000000..7554df66
--- /dev/null
+++ b/forge/tests/forge/custom-solver/custom_solver_subdir.frg
@@ -0,0 +1,9 @@
+#lang forge
+option solver "./subdir/run.sh"
+option run_sterling off
+
+sig Node {edges: set Node}
+
+test expect {
+    s: {some edges} for 1 Node is sat
+}
diff --git a/forge/tests/forge/custom-solver/custom_solver_temporal.frg b/forge/tests/forge/custom-solver/custom_solver_temporal.frg
new file mode 100644
index 00000000..bc1238c8
--- /dev/null
+++ b/forge/tests/forge/custom-solver/custom_solver_temporal.frg
@@ -0,0 +1,11 @@
+#lang forge/temporal
+option solver "./run.sh"
+option run_sterling off
+
+one sig Counter { var c: one Int }
+pred traces {
+    Counter.c = 0
+    always { Counter.c' = add[1, Counter.c]}
+}
+
+sat_traces: assert {traces} is sat for 2 Int
diff --git a/forge/tests/forge/custom-solver/run.bat b/forge/tests/forge/custom-solver/run.bat
new file mode 100644
index 00000000..6e459fa7
--- /dev/null
+++ b/forge/tests/forge/custom-solver/run.bat
@@ -0,0 +1,2 @@
+@ECHO OFF
+python3 solver.py %1
diff --git a/forge/tests/forge/custom-solver/run.sh b/forge/tests/forge/custom-solver/run.sh
new file mode 100755
index 00000000..a9a93bcb
--- /dev/null
+++ b/forge/tests/forge/custom-solver/run.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+python3 solver.py $1
diff --git a/forge/tests/forge/custom-solver/solver.py b/forge/tests/forge/custom-solver/solver.py
new file mode 100644
index 00000000..7e2a111b
--- /dev/null
+++ b/forge/tests/forge/custom-solver/solver.py
@@ -0,0 +1,18 @@
+import sys
+
+def readInput(cnfFile):
+    variables = set()
+    with open(cnfFile, "r") as f:
+        for line in f.readlines():
+            tokens = line.strip().split()
+            if tokens and tokens[0] != "p" and tokens[0] != "c":
+                for lit in tokens[:-1]:
+                    variables.add(lit.strip("-"))
+    return variables
+
+if __name__ == "__main__":
+    inputFile = sys.argv[1]
+    variables = readInput(inputFile)
+    result = " ".join(variables)
+    print(f"s SATISFIABLE")
+    print(f"v {result}")
diff --git a/forge/tests/forge/custom-solver/subdir/run.bat b/forge/tests/forge/custom-solver/subdir/run.bat
new file mode 100644
index 00000000..6e459fa7
--- /dev/null
+++ b/forge/tests/forge/custom-solver/subdir/run.bat
@@ -0,0 +1,2 @@
+@ECHO OFF
+python3 solver.py %1
diff --git a/forge/tests/forge/custom-solver/subdir/run.sh b/forge/tests/forge/custom-solver/subdir/run.sh
new file mode 100755
index 00000000..a4a29bef
--- /dev/null
+++ b/forge/tests/forge/custom-solver/subdir/run.sh
@@ -0,0 +1,4 @@
+#!/bin/bash
+
+# Python solver
+python3 solver.py $1
diff --git a/forge/tests/forge/custom-solver/win/custom_solver.frg b/forge/tests/forge/custom-solver/win/custom_solver.frg
new file mode 100644
index 00000000..df62bb2f
--- /dev/null
+++ b/forge/tests/forge/custom-solver/win/custom_solver.frg
@@ -0,0 +1,9 @@
+#lang forge
+option solver "./run.bat"
+option run_sterling off
+
+sig Node {edges: set Node}
+
+test expect {
+    s: {some edges} for 1 Node is sat
+}
diff --git a/forge/tests/forge/custom-solver/win/custom_solver_froglet.frg b/forge/tests/forge/custom-solver/win/custom_solver_froglet.frg
new file mode 100644
index 00000000..af25313e
--- /dev/null
+++ b/forge/tests/forge/custom-solver/win/custom_solver_froglet.frg
@@ -0,0 +1,9 @@
+#lang forge/froglet
+option solver "./run.bat"
+option run_sterling off
+
+sig Node {edges: lone Node}
+
+test expect {
+    s: {some n: Node | some n.edges} for 1 Node is sat
+}
diff --git a/forge/tests/forge/custom-solver/win/custom_solver_subdir.frg b/forge/tests/forge/custom-solver/win/custom_solver_subdir.frg
new file mode 100644
index 00000000..07118821
--- /dev/null
+++ b/forge/tests/forge/custom-solver/win/custom_solver_subdir.frg
@@ -0,0 +1,9 @@
+#lang forge
+option solver "./subdir/run.bat"
+option run_sterling off
+
+sig Node {edges: set Node}
+
+test expect {
+    s: {some edges} for 1 Node is sat
+}
diff --git a/forge/tests/forge/custom-solver/win/run.bat b/forge/tests/forge/custom-solver/win/run.bat
new file mode 100644
index 00000000..6e459fa7
--- /dev/null
+++ b/forge/tests/forge/custom-solver/win/run.bat
@@ -0,0 +1,2 @@
+@ECHO OFF
+python3 solver.py %1
diff --git a/forge/tests/forge/custom-solver/win/solver.py b/forge/tests/forge/custom-solver/win/solver.py
new file mode 100644
index 00000000..7e2a111b
--- /dev/null
+++ b/forge/tests/forge/custom-solver/win/solver.py
@@ -0,0 +1,18 @@
+import sys
+
+def readInput(cnfFile):
+    variables = set()
+    with open(cnfFile, "r") as f:
+        for line in f.readlines():
+            tokens = line.strip().split()
+            if tokens and tokens[0] != "p" and tokens[0] != "c":
+                for lit in tokens[:-1]:
+                    variables.add(lit.strip("-"))
+    return variables
+
+if __name__ == "__main__":
+    inputFile = sys.argv[1]
+    variables = readInput(inputFile)
+    result = " ".join(variables)
+    print(f"s SATISFIABLE")
+    print(f"v {result}")
diff --git a/forge/tests/forge/custom-solver/win/subdir/run.bat b/forge/tests/forge/custom-solver/win/subdir/run.bat
new file mode 100644
index 00000000..6e459fa7
--- /dev/null
+++ b/forge/tests/forge/custom-solver/win/subdir/run.bat
@@ -0,0 +1,2 @@
+@ECHO OFF
+python3 solver.py %1
diff --git a/forge/tests/forge/domains/crypto/test_ns.frg b/forge/tests/forge/domains/crypto/test_ns.frg
index c16d0ae3..33340600 100644
--- a/forge/tests/forge/domains/crypto/test_ns.frg
+++ b/forge/tests/forge/domains/crypto/test_ns.frg
@@ -41,19 +41,19 @@ pred ns_scenario {
 test expect {
     -- Exact bounds: baseline regression test
     ns_attack: { ns_scenario }
-        for exactly 6 Timeslot, exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
+        for exactly 6 Timeslot, exactly 2 Microtick, exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
             exactly 2 text, exactly 5 Ciphertext, exactly 1 ns_init, exactly 1 ns_resp,
             exactly 3 PublicKey, exactly 3 PrivateKey, 0 skey, exactly 6 akey, exactly 3 strand,
             6 Int
-            for {next is linear}
+            for {next is linear  mt_next is linear}
         is sat
 
     -- Non-exact bounds: exercises bounds partition and cardinality constraints
     ns_attack_nonexact: { ns_scenario }
-        for 6 Timeslot, exactly 1 KeyPairs, 6 Key, 3 name, 16 mesg,
+        for 6 Timeslot, exactly 2 Microtick, exactly 1 KeyPairs, 6 Key, 3 name, 16 mesg,
             2 text, 5 Ciphertext, exactly 1 ns_init, exactly 1 ns_resp,
             3 PublicKey, 3 PrivateKey, 0 skey, 6 akey, 3 strand,
             6 Int
-            for {next is linear}
+            for {next is linear  mt_next is linear}
         is sat
 }
diff --git a/forge/tests/forge/domains/crypto/test_ns_fixed.frg b/forge/tests/forge/domains/crypto/test_ns_fixed.frg
index 5bc5eec3..ea414797 100644
--- a/forge/tests/forge/domains/crypto/test_ns_fixed.frg
+++ b/forge/tests/forge/domains/crypto/test_ns_fixed.frg
@@ -38,10 +38,10 @@ pred ns_scenario {
 
 test expect {
     ns_fixed_no_attack: { ns_scenario }
-        for exactly 6 Timeslot, exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
+        for exactly 6 Timeslot, exactly 2 Microtick, exactly 1 KeyPairs, exactly 6 Key, exactly 3 name, 16 mesg,
             exactly 2 text, exactly 5 Ciphertext, exactly 1 ns_init, exactly 1 ns_resp,
             exactly 3 PublicKey, exactly 3 PrivateKey, 0 skey, exactly 6 akey, exactly 3 strand,
             6 Int
-            for {next is linear}
+            for {next is linear  mt_next is linear}
         is unsat
 }
diff --git a/forge/tests/forge/domains/crypto/test_reflect.frg b/forge/tests/forge/domains/crypto/test_reflect.frg
index 1f89aeb3..dc96e1f9 100644
--- a/forge/tests/forge/domains/crypto/test_reflect.frg
+++ b/forge/tests/forge/domains/crypto/test_reflect.frg
@@ -22,12 +22,12 @@ pred reflect_scenario {
 
 test expect {
     reflect_sat: { reflect_scenario }
-        for exactly 4 Timeslot, 13 mesg,
+        for exactly 4 Timeslot, exactly 2 Microtick, 13 mesg,
             exactly 1 KeyPairs, exactly 6 Key, exactly 6 akey, 0 skey,
             exactly 3 PrivateKey, exactly 3 PublicKey,
             exactly 3 name, 0 text, exactly 4 Ciphertext,
             exactly 1 reflect_init, exactly 1 reflect_resp,
             1 Int
-            for {next is linear}
+            for {next is linear  mt_next is linear}
         is sat
 }
diff --git a/forge/tests/forge/other/ast-errors.frg b/forge/tests/forge/other/ast-errors.frg
index b20c6965..d09ec260 100644
--- a/forge/tests/forge/other/ast-errors.frg
+++ b/forge/tests/forge/other/ast-errors.frg
@@ -238,6 +238,9 @@ test expect {
     -- Nothing to do with priming; this one should give an empty-join error
     non_equiv4: {some x: Thread | baseline[x] != World.(loc[x])} 
       is forge_error
-    non_equiv5: {some x: Thread | baseline[x] != (World.loc[x])'} 
+    non_equiv5: {some x: Thread | baseline[x] != (World.loc[x])'}
       is unsat
+
+    prime_nonvar_comprehension: { some {t: Thread | some t}' }
+      is forge_error "Prime operator used in non-temporal context"
 }
diff --git a/forge/utils/collector.rkt b/forge/utils/collector.rkt
index a9672af0..bebfa9c1 100644
--- a/forge/utils/collector.rkt
+++ b/forge/utils/collector.rkt
@@ -28,8 +28,9 @@
 ; gives the initial value of that context, defaulting to #f.
 
 ; Also, the ordering of internal traversals is consistent, but not adjustable:
-; e.g., a quantified formula will always produce
-;   (append <new variables> <collected from domains> <collected from inner formula>)
+; e.g., a quantified formula will interleave variable and domain results in
+; declaration order, followed by results from the inner formula. Variables are
+; only included if accepted by the matcher function.
 
 ; Finally, duplicates will not be removed. E.g., collecting on (& iden iden) will
 ; produce `iden` twice in the resulting list unless the matcher prevents it.
@@ -220,23 +221,40 @@
     [(node/int/sum-quant info decls int-expr)
      (process-quant-shaped-node expr decls int-expr quantvars matcher order collected stop context get-new-context)]))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Used by quantified formulas, set comprehensions, and integer-sum expressions.
+;; Each quantifier variable is visited through the matcher (rather than being
+;; unconditionally included).
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
 (: process-quant-shaped-node (-> node Decls node (Listof node/expr/quantifier-var) (-> node Any Any) Symbol
                                  (Listof Any) (-> node Any Boolean) Any
                                  (-> node Any Any) (Listof Any)))
 (define (process-quant-shaped-node node decls inner-node quantvars matcher order collected stop context get-new-context)
-  (define new-vs-and-collected
-    (for/fold ([vs-and-collected : (List (Listof node/expr/quantifier-var) (Listof Any)) (list '() '())])
+  (define-values (new-vs domain-collected)
+    (for/fold ([curr-new-quantvars : (Listof node/expr/quantifier-var) '()]
+               [curr-domain-collected : (Listof Any) '()])
               ([decl decls])
-      (define curr-new-quantvars (first vs-and-collected))
+
+      ;; Visit the quantifier variable through the matcher
+      (define collected-this-quantvar
+        (visit (car decl) curr-new-quantvars
+               matcher order collected stop context get-new-context))
+
+      ;; Accumulate this variable for subsequent domain/body context
       (define new-quantvars (cons (car decl) curr-new-quantvars))
+
+      ;; Visit the domain expression with all previously-declared variables as context
       (define new-domain-collected
-        (visit (cdr decl) (append curr-new-quantvars new-quantvars) matcher order collected stop context get-new-context))         
-      (list new-quantvars (append (second vs-and-collected) new-domain-collected))))
-  
-  (define new-quantvars (reverse (first new-vs-and-collected)))
-  (define new-domain-collected (second new-vs-and-collected))
+        (visit (cdr decl) (append curr-new-quantvars new-quantvars)
+               matcher order collected stop context get-new-context))
+
+      (values new-quantvars
+              (append curr-domain-collected collected-this-quantvar new-domain-collected))))
+
+  (define new-quantvars (reverse new-vs))
   (define inner-collected (visit inner-node new-quantvars matcher order collected stop context get-new-context))
-  (append new-quantvars new-domain-collected inner-collected))
+  (append domain-collected inner-collected))
 
 (: interpret-int-op (-> node/int/op (Listof node/expr/quantifier-var) (Listof node) (-> node Any Any) Symbol
                         (Listof Any) (-> node Any Boolean) Any
@@ -292,7 +310,15 @@
     (check-equal?
      (collect fmla
               (lambda (n ctxt) (if (node/expr? n) n #f)) #:order 'pre-order)
-     (list v univ (&/func (->/func v v) iden) (->/func v v) v v iden)))
+     (list v univ (&/func (->/func v v) iden) (->/func v v) v v iden))
+
+    ;; Confirm that quantified variables are excluded when the matcher rejects them
+    (check-equal?
+     (collect fmla
+              (lambda (n ctxt) (if (and (node/expr? n)
+                                        (not (node/expr/quantifier-var? n))) n #f))
+              #:order 'pre-order)
+     (list univ (&/func (->/func v v) iden) (->/func v v) iden)))
 
   ; Confirm that multi-decl extraction works for the complex quantifier-shaped cases
   ; which all invoke the process-quant-shaped-node helper
@@ -307,8 +333,8 @@
     (check-equal?
      (collect expr (lambda (n ctxt) (if (node/expr? n) n #f)) #:order 'pre-order)
      (list expr
-           v1 v2
-           univ (&/func univ univ) univ univ
+           v1 univ
+           v2 (&/func univ univ) univ univ
            (&/func (->/func v1 v2) iden) (->/func v1 v2) v1 v2 iden)))
 
   ; Confirm that the stop policy is respected.