From 7f1d49854ee1a761e9725e1196dba201a6df11ec Mon Sep 17 00:00:00 2001
From: Emina Torlak <emina@alum.mit.edu>
Date: Wed, 3 Feb 2021 15:07:04 -0800
Subject: [PATCH] Rename spec? -> vc? and spec-* -> vc-*.

---
 rosette/base/base.rkt                         |   2 +-
 rosette/base/core/bool.rkt                    | 117 ++++++++---------
 .../scribble/essentials/essentials-log.txt    |  38 +++---
 .../scribble/essentials/essentials.scrbl      |  20 +--
 .../scribble/forms/rosette-forms-log.txt      |  44 +++----
 .../guide/scribble/forms/rosette-forms.scrbl  |  20 +--
 rosette/lib/trace/tool.rkt                    |   4 +-
 rosette/query/form.rkt                        |  14 +-
 sdsl/bv/lang/core.rkt                         |   6 +-
 test/base/bitvector.rkt                       |   6 +-
 test/base/bvlib.rkt                           |  12 +-
 test/base/eval-guarded.rkt                    |  10 +-
 test/base/finitize.rkt                        |   2 +-
 test/base/real.rkt                            |  12 +-
 test/base/vc.rkt                              | 120 +++++++++---------
 test/cplex/solve.rkt                          |   2 +-
 16 files changed, 215 insertions(+), 214 deletions(-)

diff --git a/rosette/base/base.rkt b/rosette/base/base.rkt
index 6455df51..273e9492 100644
--- a/rosette/base/base.rkt
+++ b/rosette/base/base.rkt
@@ -16,7 +16,7 @@
   (filtered-out drop@ 
     (combine-out
      ; core/bool.rkt
-     vc with-vc vc-clear! spec? vc-true? vc-true spec-assumes spec-asserts
+     vc with-vc vc-clear! vc? vc-true? vc-true vc-assumes vc-asserts
      @assert @assume
      @boolean? @false? @! @&& @=> @<=> @forall @exists
      ; core/real.rkt
diff --git a/rosette/base/core/bool.rkt b/rosette/base/core/bool.rkt
index 3b505623..939954dd 100644
--- a/rosette/base/core/bool.rkt
+++ b/rosette/base/core/bool.rkt
@@ -9,8 +9,8 @@
  and-&& or-|| instance-of? T*->boolean?
  ;; ---- VC generation ---- ;;       
  @assert @assume $assert $assume
- (rename-out [vc-get vc]) vc-clear! with-vc vc-merge!
- spec? spec-assumes spec-asserts
+ (rename-out [vc-get vc]) vc-clear! vc-merge! with-vc 
+ vc? vc-assumes vc-asserts
  vc-true vc-true?)
 
 ;; ----------------- Boolean type ----------------- ;; 
@@ -287,36 +287,38 @@
 
 ;; ----------------- VC generation ----------------- ;;
 
-; A spec consists of two (symbolic or concrete) @boolean?
-; values representing the assumptions and assertions issued
-; so far. A spec is legal if at least one of its assumes or
-; asserts is true under all models.
-(struct spec (assumes asserts) #:transparent)
+; A verification condition (VC) consists of two @boolean?
+; values representing assumptions and assertions issued
+; during execution. A VC is legal if at least one of its
+; constituent fields is true under all models.
 
-; The true (top) spec.
-(define vc-true (spec #t #t))
+(struct vc (assumes asserts) #:transparent)
+
+; The true verification condition.
+(define vc-true (vc #t #t))
 
 (define (vc-true? s) (equal? s vc-true))
 
-; Returns (spec (s.assumes && (s.asserts => g) s.asserts). 
+; Returns (vc (s.assumes && (s.asserts => g)) s.asserts). 
 (define (assuming s g)  ; g must be a symbolic or concrete boolean
-  (spec (&& (spec-assumes s) (=> (spec-asserts s) g)) (spec-asserts s)))
+  (vc (&& (vc-assumes s) (=> (vc-asserts s) g)) (vc-asserts s)))
 
-; Returns (spec s.assumes (s.asserts && (s.assumes => g))). 
+; Returns (vc s.assumes (s.asserts && (s.assumes => g))). 
 (define (asserting s g) ; g must be a symbolic or concrete boolean 
-  (spec (spec-assumes s) (&& (spec-asserts s) (=> (spec-assumes s) g))))
+  (vc (vc-assumes s) (&& (vc-asserts s) (=> (vc-assumes s) g))))
 
-; The vc parameter keeps track of the current verification condition,
-; which is an instance of spec?. The default vc is the true spec.
-(define vc (make-parameter
-            vc-true
-            (lambda (v) (unless (spec? v) (raise-argument-error 'vc "spec?" v)) v)))
+; The current-vc parameter keeps track of the current verification condition,
+; which is an instance of vc?. The default value for this parameter is vc-true.
+(define current-vc
+  (make-parameter
+   vc-true
+   (lambda (v) (unless (vc? v) (raise-argument-error 'vc "vc?" v)) v)))
 
 ; Returns the current vc, without exposing the parameter outside the module. 
-(define (vc-get) (vc))
+(define (vc-get) (current-vc))
 
 ; Clears the current vc by setting it to the true spec.
-(define (vc-clear!) (vc vc-true))
+(define (vc-clear!) (current-vc vc-true))
 
 ; Returns #t if x && (g => y) is equivalent to x according to the embedded
 ; rewrite rules. Otherwise returns #f.
@@ -355,48 +357,48 @@
 ;     (apply && gs=>ys)]
 ;    [_ (apply && xf gs=>ys)]))
 
-; Takes as input a list of n guards and n specs and sets the current vc
-; to (vc) && (spec-guard guard1 specs1) && ... && (spec-guard guardn specn).
-; Then, it checks if either the assumes or the asserts of the resulting spec
+; Takes as input a list of n guards and n vcs and sets the current vc
+; to (current-vc) && (vc-guard guard1 vc1) && ... && (vc-guard guardn vcn).
+; Then, it checks if either the assumes or the asserts of the resulting vc
 ; are false? and if so, throws either an exn:fail:svm:assume? or
 ; exn:fail:svm:assert? exception. This procedure makes the following assumptions:
 ; * at most one of the given guards is true in any model,
-; * (spec-assumes specs[i]) => (spec-assumes (vc)) for all i, and 
-; * (spec-asserts specs[i]) => (spec-asserts (vc)) for all i.
-(define (vc-merge! guards specs)
-  (unless (null? specs)
-    (define specm
-      (spec (merge-field spec-assumes (vc) guards specs)
-            (merge-field spec-asserts (vc) guards specs)))
-    (vc specm)
-    (when (false? (spec-assumes specm))
+; * (vc-assumes specs[i]) => (vc-assumes (current-vc)) for all i, and 
+; * (vc-asserts specs[i]) => (vc-asserts (current-vc)) for all i.
+(define (vc-merge! guards vcs)
+  (unless (null? vcs)
+    (define vc*
+      (vc (merge-field vc-assumes (current-vc) guards vcs)
+          (merge-field vc-asserts (current-vc) guards vcs)))
+    (current-vc vc*)
+    (when (false? (vc-assumes vc*))
       (raise-exn:fail:svm:assume:core "contradiction"))
-    (when (false? (spec-asserts specm))
+    (when (false? (vc-asserts vc*))
       (raise-exn:fail:svm:assert:core "contradiction"))))
 
-; Sets the current vc to (spec-proc (vc) g) where g is (@true? val).
-; If g is #f or the resulting vc's spec-field value is #f,
+; Sets the current vc to (vc-proc (current-vc) g) where g is (@true? val).
+; If g is #f or the resulting vc's vc-field value is #f,
 ; uses raise-exn throws an exn:fail:svm exception. 
-(define-syntax-rule (vc-set! val msg spec-proc spec-field raise-exn)
+(define-syntax-rule (vc-set! val msg vc-proc vc-field raise-exn)
   (let* ([guard (@true? val)]
-         [specg (spec-proc (vc) guard)])
-    (vc specg)
+         [vc* (vc-proc (current-vc) guard)])
+    (current-vc vc*)
     (when (false? guard)
       (raise-exn msg))
-    (when (false? (spec-field specg))
+    (when (false? (vc-field vc*))
       (raise-exn "contradiction"))))
 
-; Sets the current vc to (asserting (vc) g) where g is (@true? val).
+; Sets the current vc to (asserting (current-vc) g) where g is (@true? val).
 ; If g is #f or the resulting vc's asserts field is #f, throws an
 ; exn:fail:svm:assert exception of the given kind.  
 (define-syntax-rule (vc-assert! val msg raise-kind)
-  (vc-set! val msg asserting spec-asserts raise-kind))
+  (vc-set! val msg asserting vc-asserts raise-kind))
 
-; Sets the current vc to (assuming (vc) g) where g is (@true? val).
+; Sets the current vc to (assuming (current-vc) g) where g is (@true? val).
 ; If g is #f or the resulting vc's assumes field is #f, throws an
 ; exn:fail:svm:assume exception of the given kind. 
 (define-syntax-rule (vc-assume! val msg raise-kind)
-  (vc-set! val msg assuming spec-assumes raise-kind))
+  (vc-set! val msg assuming vc-assumes raise-kind))
 
 ; The $assert form has three variants: ($assert val), ($assert val msg),
 ; and ($assert val msg kind), where val is the value being asserted, msg
@@ -406,7 +408,7 @@
 ; The first two variants of this form are used for issuing assertions from
 ; within the Rosette core. The third variant is used to implement the @assert
 ; form that is exposed to user code. An $assert call modifies the current vc to
-; reflect the issued assertion. If the issued assertion or the spec-assert of the
+; reflect the issued assertion. If the issued assertion or the vc-assert of the
 ; current vc reduce to #f, the call throws an exception of the given kind after
 ; updating the vc.
 (define-syntax ($assert stx)
@@ -442,38 +444,37 @@
     [(_ val msg) (syntax/loc stx ($assume val msg raise-exn:fail:svm:assume:user))]))
 
 (define (halt-svm ex)
-  (define result (halt ex (vc)))
+  (define result (halt ex (current-vc)))
   ((current-reporter) 'exception result)
   result)
 
 (define (halt-err ex) ; Treat an exn:fail? error as an assertion failure.
   (define result
     (halt (make-exn:fail:svm:assert:err (exn-message ex) (exn-continuation-marks ex))
-          (asserting (vc) #f)))
+          (asserting (current-vc) #f)))
   ((current-reporter) 'exception result)
   result)
 
 ; The with-vc form has two variants, (with-vc body) and (with-vc vc0 body).
-; The former expands into (with-vc (vc) body). The latter sets the current
-; vc to vc0, evaluates the given body, returns the result, and reverts vc
+; The former expands into (with-vc (current-vc) body). The latter sets the current
+; vc to vc0, evaluates the given body, returns the result, and reverts current-vc
 ; to the value it held before the call to with-vc.
 ;
 ; If the evaluation of the body terminates normally, (with-vc vc0 body)
-; outputs (ans v s) where v is the value computed by the body, and s is 
-; the specification (i.e., assumes and asserts) generated during the evaluation,
-; with v0 as the initial specification. 
+; outputs (ans v vc*) where v is the value computed by the body, and vc* is 
+; the vc (i.e., assumes and asserts) generated during the evaluation,
+; with vc0 as the initial vc. 
 ;
 ; If the evaluation of the body terminates abnormally with an exn:fail? exception,
-; (with-vc vc0 body) outputs (halt v s) where v is an exn:fail:svm? exception
-; that represents the cause of the abnormal termination, and s is the specification
-; (i.e., assumes and asserts) generated during the evaluation, with v0 as
-; the initial specification.
+; (with-vc vc0 body) outputs (halt v vc*) where v is an exn:fail:svm? exception
+; that represents the cause of the abnormal termination, and vc* is the vc
+; generated during the evaluation, with vc0 as the initial vc.
 (define-syntax (with-vc stx)
   (syntax-case stx ()
-    [(_ body) (syntax/loc stx (with-vc (vc) body))]
+    [(_ body) (syntax/loc stx (with-vc (current-vc) body))]
     [(_ vc0 body)
      (syntax/loc stx
-       (parameterize ([vc vc0])
+       (parameterize ([current-vc vc0])
          (with-handlers ([exn:fail:svm? halt-svm]
                          [exn:fail?     halt-err])
-           (ans body (vc)))))]))
+           (ans body (current-vc)))))]))
diff --git a/rosette/guide/scribble/essentials/essentials-log.txt b/rosette/guide/scribble/essentials/essentials-log.txt
index 5c4fd22c..2a6eb91f 100644
--- a/rosette/guide/scribble/essentials/essentials-log.txt
+++ b/rosette/guide/scribble/essentials/essentials-log.txt
@@ -79,11 +79,11 @@
  #"")
 ((assert #t) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((assert #f) ((3) 0 () 0 () () (q exn "[assert] failed")) #"" #"")
-((spec-asserts (vc)) ((3) 0 () 0 () () (q values #f)) #"" #"")
+((vc-asserts (vc)) ((3) 0 () 0 () () (q values #f)) #"" #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-asserts (vc)) ((3) 0 () 0 () () (q values #t)) #"" #"")
+((vc-asserts (vc)) ((3) 0 () 0 () () (q values #t)) #"" #"")
 ((assert (not b)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-asserts (vc))
+((vc-asserts (vc))
  ((3)
   1
   (((lib "rosette/guide/scribble/util/lifted.rkt")
@@ -97,13 +97,13 @@
  #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((assume #t) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-assumes (vc)) ((3) 0 () 0 () () (q values #t)) #"" #"")
+((vc-assumes (vc)) ((3) 0 () 0 () () (q values #t)) #"" #"")
 ((assume #f) ((3) 0 () 0 () () (q exn "[assume] failed")) #"" #"")
-((spec-assumes (vc)) ((3) 0 () 0 () () (q values #f)) #"" #"")
+((vc-assumes (vc)) ((3) 0 () 0 () () (q values #f)) #"" #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((define-symbolic i j integer?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((assume (> j 0)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-assumes (vc))
+((vc-assumes (vc))
  ((3)
   1
   (((lib "rosette/guide/scribble/util/lifted.rkt")
@@ -116,7 +116,7 @@
  #""
  #"")
 ((assert (< (- i j) i)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
-((spec-asserts (vc))
+((vc-asserts (vc))
  ((3)
   1
   (((lib "rosette/guide/scribble/util/lifted.rkt")
@@ -130,7 +130,7 @@
  #"")
 ((pretty-print (vc))
  ((3) 0 () 0 () () (c values c (void)))
- #"(spec (< 0 j) (|| (! (< 0 j)) (< (+ i (- j)) i)))\n"
+ #"(vc (< 0 j) (|| (! (< 0 j)) (< (+ i (- j)) i)))\n"
  #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((define int32? (bitvector 32)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -422,7 +422,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x394f0402 32)]\n [h (bv #x529e7c00 32)])"))))
- #"cpu time: 1 real time: 38 gc time: 0\n"
+ #"cpu time: 2 real time: 38 gc time: 0\n"
  #"")
 ((time (verify (check-mid-slow bvmid l h)))
  ((3)
@@ -437,7 +437,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x2faef9a1 32)]\n [h (bv #x5eefb8dd 32)])"))))
- #"cpu time: 4 real time: 183 gc time: 0\n"
+ #"cpu time: 3 real time: 174 gc time: 0\n"
  #"")
 ((time (verify (check-mid bvmid-no-overflow l h)))
  ((3)
@@ -449,7 +449,7 @@
   ()
   ()
   (c values c (0 (u . "(unsat)"))))
- #"cpu time: 1 real time: 159 gc time: 0\n"
+ #"cpu time: 1 real time: 156 gc time: 0\n"
  #"")
 ((error 'call-with-deep-time-limit "out of time")
  ((3) 0 () 0 () () (q exn "call-with-deep-time-limit: out of time"))
@@ -470,7 +470,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x00000001 32)]\n [h (bv #x7fffffff 32)])"))))
- #"cpu time: 3 real time: 24 gc time: 0\n"
+ #"cpu time: 3 real time: 25 gc time: 0\n"
  #"")
 ((time (verify (check-mid-slow bvmid-no-overflow l h)))
  ((3)
@@ -482,7 +482,7 @@
   ()
   ()
   (c values c (0 (u . "(unsat)"))))
- #"cpu time: 1 real time: 159 gc time: 0\n"
+ #"cpu time: 1 real time: 155 gc time: 0\n"
  #"")
 ((current-bitwidth 32) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((time (verify (check-mid-slow bvmid l h)))
@@ -510,7 +510,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x71979fa3 32)]\n [h (bv #x76b91b88 32)])"))))
- #"cpu time: 1 real time: 151 gc time: 0\n"
+ #"cpu time: 1 real time: 150 gc time: 0\n"
  #"")
 ((current-bitwidth 512) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((time (verify (check-mid-slow bvmid l h)))
@@ -526,7 +526,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x70000006 32)]\n [h (bv #x73fffffa 32)])"))))
- #"cpu time: 1 real time: 381 gc time: 0\n"
+ #"cpu time: 1 real time: 377 gc time: 0\n"
  #"")
 ((time (verify (check-mid-slow bvmid-no-overflow l h)))
  ((3)
@@ -538,7 +538,7 @@
   ()
   ()
   (c values c (0 (u . "(unsat)"))))
- #"cpu time: 1 real time: 438 gc time: 0\n"
+ #"cpu time: 1 real time: 428 gc time: 0\n"
  #"")
 ((current-bitwidth #f) ((3) 0 () 0 () () (c values c (void))) #"" #"")
 ((require rosette/solver/smt/z3)
@@ -562,7 +562,7 @@
    values
    c
    (0 (u . "(model\n [l (bv #x394f0402 32)]\n [h (bv #x529e7c00 32)])"))))
- #"cpu time: 5 real time: 36 gc time: 0\n"
+ #"cpu time: 4 real time: 34 gc time: 0\n"
  #"")
 ((time (verify (check-mid-slow bvmid l h)))
  ((3)
@@ -749,7 +749,7 @@
  #"")
 ((define cex (time (verify (check-sqrt bvsqrt l))))
  ((3) 0 () 0 () () (c values c (void)))
- #"cpu time: 6 real time: 1039 gc time: 0\n"
+ #"cpu time: 7 real time: 1019 gc time: 0\n"
  #"")
 ((bvsqrt (evaluate l cex))
  ((3) 0 () 0 () () (q exn "[assert] Out of fuel."))
@@ -767,5 +767,5 @@
   ()
   ()
   (c values c (0 (u . "(unsat)"))))
- #"cpu time: 15 real time: 69086 gc time: 10\n"
+ #"cpu time: 4 real time: 67739 gc time: 0\n"
  #"")
diff --git a/rosette/guide/scribble/essentials/essentials.scrbl b/rosette/guide/scribble/essentials/essentials.scrbl
index 0d1294e5..d39c3cf9 100644
--- a/rosette/guide/scribble/essentials/essentials.scrbl
+++ b/rosette/guide/scribble/essentials/essentials.scrbl
@@ -3,7 +3,7 @@
 @(require (for-label racket (only-in racket/sandbox with-deep-time-limit))
           (for-label  
            rosette/base/form/define
-           (only-in rosette/base/base assert assume vc spec-asserts spec-assumes vc-clear!)
+           (only-in rosette/base/base assert assume vc vc-asserts vc-assumes vc-clear!)
            rosette/query/query  
            (only-in rosette/base/base bv? bitvector
                     bvsdiv bvadd bvsle bvsub bvand
@@ -111,11 +111,11 @@ Like many languages, Rosette provides a construct for expressing @emph{assertion
 When given a symbolic boolean value, however, a Rosette assertion has no immediate effect.  Instead, the value is accumulated in the current @tech[#:key "vc"]{verification condition} (VC), and the assertion's effect (whether it passes or fails) is eventually determined by the solver.
 
 @examples[#:eval rosette-eval #:label #f
-(code:line (spec-asserts (vc)) (code:comment "We asserted #f above, so the current VC reflects that."))
-(code:line (vc-clear!)         (code:comment "Clear the current VC."))
-(spec-asserts (vc))
-(code:line (assert (not b))    (code:comment "Add the assertion (not b) to the VC."))
-(spec-asserts (vc))
+(code:line (vc-asserts (vc)) (code:comment "We asserted #f above, so the current VC reflects that."))
+(code:line (vc-clear!)       (code:comment "Clear the current VC."))
+(vc-asserts (vc))
+(code:line (assert (not b))  (code:comment "Add the assertion (not b) to the VC."))
+(vc-asserts (vc))
 (vc-clear!)]
 
 Assertions express properties that a program must satisfy on all @emph{legal} inputs. In Rosette, as in other solver-aided frameworks, we use @emph{assumptions} to describe which inputs are legal. If a program violates an assertion on a legal input, we blame the program. But if it violates an assertion on an illegal input, we blame the caller. In other words, a program is considered incorrect only when it violates an assertion on a legal input.
@@ -124,17 +124,17 @@ Assumptions behave analogously to assertions on both concrete and symbolic value
 
 @examples[#:eval rosette-eval #:label #f
 (assume #t)
-(spec-assumes (vc))
+(vc-assumes (vc))
 (eval:alts
  (code:line (assume #f)         (code:comment "Assuming #f aborts the execution with an exception."))
  (eval:error (assume #f)))
-(spec-assumes (vc))
+(vc-assumes (vc))
 (vc-clear!)
 (define-symbolic i j integer?)
 (code:line (assume (> j 0))     (code:comment "Add the assumption (> j 0) to the VC."))
-(spec-assumes (vc))
+(vc-assumes (vc))
 (assert (< (- i j) i))
-(code:line (spec-asserts (vc))  (code:comment "The assertions must hold when the assumptions hold."))
+(code:line (vc-asserts (vc))    (code:comment "The assertions must hold when the assumptions hold."))
 (code:line (pretty-print (vc))  (code:comment "VC tracks the assumptions and the assertions."))]
 
 @(rosette-eval '(vc-clear!))
diff --git a/rosette/guide/scribble/forms/rosette-forms-log.txt b/rosette/guide/scribble/forms/rosette-forms-log.txt
index 668ab475..1b5e9632 100644
--- a/rosette/guide/scribble/forms/rosette-forms-log.txt
+++ b/rosette/guide/scribble/forms/rosette-forms-log.txt
@@ -166,7 +166,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((define-symbolic x boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -180,7 +180,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t x)"))))
+  (c values c (0 (u . "#(struct:vc #t x)"))))
  #""
  #"")
 ((assert #f "bad value")
@@ -196,7 +196,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #f)"))))
+  (c values c (0 (u . "#(struct:vc #t #f)"))))
  #""
  #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -209,7 +209,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((vc)
@@ -221,7 +221,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((assume #t) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -235,7 +235,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((define-symbolic x boolean?) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -249,7 +249,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec x #t)"))))
+  (c values c (0 (u . "#(struct:vc x #t)"))))
  #""
  #"")
 ((assume #f "bad value")
@@ -265,7 +265,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #f #t)"))))
+  (c values c (0 (u . "#(struct:vc #f #t)"))))
  #""
  #"")
 ((vc-clear!) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -278,7 +278,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((define-symbolic a b c d boolean?)
@@ -294,7 +294,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((verify (assert a))
@@ -318,7 +318,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((assume a) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -332,7 +332,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec a (|| b (! a)))"))))
+  (c values c (0 (u . "#(struct:vc a (|| b (! a)))"))))
  #""
  #"")
 ((verify (begin (assume c) (assert d)))
@@ -356,7 +356,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec a (|| b (! a)))"))))
+  (c values c (0 (u . "#(struct:vc a (|| b (! a)))"))))
  #""
  #"")
 ((verify (assert a))
@@ -381,7 +381,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((verify (assert a))
@@ -407,7 +407,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((synthesize
@@ -435,7 +435,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((assume (odd? x)) ((3) 0 () 0 () () (c values c (void))) #"" #"")
@@ -448,7 +448,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec (! (= 0 (remainder x 2))) #t)"))))
+  (c values c (0 (u . "#(struct:vc (! (= 0 (remainder x 2))) #t)"))))
  #""
  #"")
 ((synthesize #:forall (list x) #:guarantee (assert (odd? (+ x c))))
@@ -472,7 +472,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec (! (= 0 (remainder x 2))) #t)"))))
+  (c values c (0 (u . "#(struct:vc (! (= 0 (remainder x 2))) #t)"))))
  #""
  #"")
 ((synthesize
@@ -501,7 +501,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((synthesize
@@ -532,7 +532,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec x #t)"))))
+  (c values c (0 (u . "#(struct:vc x #t)"))))
  #""
  #"")
 ((solve (assert y))
@@ -556,7 +556,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec x #t)"))))
+  (c values c (0 (u . "#(struct:vc x #t)"))))
  #""
  #"")
 ((solve (assert (not x)))
@@ -581,7 +581,7 @@
   0
   ()
   ()
-  (c values c (0 (u . "#(struct:spec #t #t)"))))
+  (c values c (0 (u . "#(struct:vc #t #t)"))))
  #""
  #"")
 ((solve (assert (not x)))
diff --git a/rosette/guide/scribble/forms/rosette-forms.scrbl b/rosette/guide/scribble/forms/rosette-forms.scrbl
index 6b5f9ab8..5890f739 100644
--- a/rosette/guide/scribble/forms/rosette-forms.scrbl
+++ b/rosette/guide/scribble/forms/rosette-forms.scrbl
@@ -6,7 +6,7 @@
            rosette/base/core/term 
            (only-in rosette/query/finitize current-bitwidth)
            (only-in rosette/base/base
-                    assert assume vc spec-asserts spec-assumes vc-clear!
+                    assert assume vc vc-asserts vc-assumes vc-clear!
                     bv? forall)
            (only-in rosette/base/core/function function? ~>)
            (only-in rosette/base/core/reflect symbolics))
@@ -184,8 +184,8 @@ describes the corresponding syntactic constructs in detail.
 
  Formally,
  @racket[(verify expr)] searches for a model of the formula
- @racket[(spec-assumes #, @var{P})] ∧ @racket[(spec-asserts #, @var{P})] ∧
- @racket[(spec-assumes #, @var{Q})] ∧ ¬ @racket[(spec-asserts #, @var{Q})],
+ @racket[(vc-assumes #, @var{P})] ∧ @racket[(vc-asserts #, @var{P})] ∧
+ @racket[(vc-assumes #, @var{Q})] ∧ ¬ @racket[(vc-asserts #, @var{Q})],
  where @var{P} is the verification condition before the
  call to @racket[verify] and @var{Q} is the verification condition
  generated by evaluating @racket[expr].
@@ -247,9 +247,9 @@ describes the corresponding syntactic constructs in detail.
  the formula
  ∃ @var{H}. (∃ @var{I}. @var{pre}(@var{H}, @var{I})) ∧
  (∀ @var{I}. @var{pre}(@var{H}, @var{I}) ⇒ @var{post}(@var{H}, @var{I})),
- where @var{pre}(@var{H}, @var{I}) is @racket[(spec-assumes #, @var{P})] ∧
- @racket[(spec-asserts #, @var{P})] ∧ @racket[(spec-assumes #, @var{Q})],
- @var{post}(@var{H}, @var{I}) is @racket[(spec-asserts #, @var{Q})],
+ where @var{pre}(@var{H}, @var{I}) is @racket[(vc-assumes #, @var{P})] ∧
+ @racket[(vc-asserts #, @var{P})] ∧ @racket[(vc-assumes #, @var{Q})],
+ @var{post}(@var{H}, @var{I}) is @racket[(vc-asserts #, @var{Q})],
  @var{P} is the verification condition accumulated before the evaluation of 
  @racket[expr], and @var{Q} is the verification condition
  generated by evaluating @racket[expr]. This formula is stronger than the
@@ -324,8 +324,8 @@ describes the corresponding syntactic constructs in detail.
  
  Formally,
  @racket[(solve expr)] searches for a model of the formula
- @racket[(spec-assumes #, @var{P})] ∧ @racket[(spec-asserts #, @var{P})] ∧
- @racket[(spec-assumes #, @var{Q})] ∧ @racket[(spec-asserts #, @var{Q})],
+ @racket[(vc-assumes #, @var{P})] ∧ @racket[(vc-asserts #, @var{P})] ∧
+ @racket[(vc-assumes #, @var{Q})] ∧ @racket[(vc-asserts #, @var{Q})],
  where @var{P} is the verification condition before the
  call to @racket[solve] and @var{Q} is the verification condition
  generated by evaluating @racket[expr].
@@ -412,8 +412,8 @@ subsequent calls to the procedure throw an exception.
  
  Formally,
  @racket[(solve expr)] searches for an optimal model of the formula
- @racket[(spec-assumes #, @var{P})] ∧ @racket[(spec-asserts #, @var{P})] ∧
- @racket[(spec-assumes #, @var{Q})] ∧ @racket[(spec-asserts #, @var{Q})],
+ @racket[(vc-assumes #, @var{P})] ∧ @racket[(vc-asserts #, @var{P})] ∧
+ @racket[(vc-assumes #, @var{Q})] ∧ @racket[(vc-asserts #, @var{Q})],
  where @var{P} is the verification condition before the
  evaluation of @racket[expr], @var{Q} is the verification condition
  generated by evaluating @racket[expr], the cost terms @racket[min-expr] are
diff --git a/rosette/lib/trace/tool.rkt b/rosette/lib/trace/tool.rkt
index c4fdea40..660a13de 100644
--- a/rosette/lib/trace/tool.rkt
+++ b/rosette/lib/trace/tool.rkt
@@ -64,8 +64,8 @@
 (define reporter
   (match-lambda*
     [(list 'exception (halt e s))
-     (define assumes (spec-assumes s))
-     (define asserts (spec-asserts s))
+     (define assumes (vc-assumes s))
+     (define asserts (vc-asserts s))
      (define skip?
        (or (exn:fail:svm:merge? e)
            ;; We skip exn:fail:svm:merge? because we already present data of
diff --git a/rosette/query/form.rkt b/rosette/query/form.rkt
index fa03fd0e..099a253e 100644
--- a/rosette/query/form.rkt
+++ b/rosette/query/form.rkt
@@ -3,14 +3,14 @@
 (require "core.rkt" 
          (only-in "../base/core/reflect.rkt" symbolics)
          (only-in "../base/core/result.rkt" result-state)
-         (only-in "../base/core/bool.rkt" ! vc with-vc spec-assumes spec-asserts vc-true))
+         (only-in "../base/core/bool.rkt" ! vc with-vc vc-assumes vc-asserts vc-true))
 
 (provide solve verify synthesize optimize
          current-solver (rename-out [∃-solve+ solve+]))
 
 (define (pre)
   (define s (vc))
-  (list (spec-assumes s) (spec-asserts s)))
+  (list (vc-assumes s) (vc-asserts s)))
 
 (define-syntax-rule (query-vc expr)
   (result-state (with-vc vc-true expr)))
@@ -24,7 +24,7 @@
 ; (vc) is unchanged after solve returns.
 (define-syntax-rule (solve expr)
   (let ([post (query-vc expr)])
-    (∃-solve `(,@(pre) ,(spec-assumes post) ,(spec-asserts post)))))
+    (∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)))))
                
 
 ; The (verify expr) query evaluates expr, gathers all 
@@ -38,7 +38,7 @@
 ; verify returns.
 (define-syntax-rule (verify expr)
   (let ([post (query-vc expr)])
-    (∃-solve `(,@(pre) ,(spec-assumes post) ,(! (spec-asserts post))))))
+    (∃-solve `(,@(pre) ,(vc-assumes post) ,(! (vc-asserts post))))))
 
 ; The (synthesize vars expr) query evaluates the given forms, gathers all  
 ; assumptions and assertions generated during the evaluation, 
@@ -56,7 +56,7 @@
     [(_ #:forall inputs #:guarantee expr)
      (let ([vars (symbolics inputs)] ; evaluate inputs first to add their spec to (vc)
            [post (query-vc expr)])
-       (∃∀-solve vars `(,@(pre) ,(spec-assumes post)) `(,(spec-asserts post))))]
+       (∃∀-solve vars `(,@(pre) ,(vc-assumes post)) `(,(vc-asserts post))))]
     [(_ inputs expr)
      (synthesize #:forall inputs #:guarantee expr)]))
 
@@ -75,9 +75,9 @@
     [(_ kw opt #:guarantee expr)
      (let ([obj opt]    ; evaluate objective first to add its spec to (vc)
            [post (query-vc expr)])
-       (∃-solve `(,@(pre) ,(spec-assumes post) ,(spec-asserts post)) kw obj))]
+       (∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw obj))]
     [(_ kw1 opt1 kw2 opt2 #:guarantee expr)
      (let ([obj1 opt1]  ; evaluate objectives first to add their spec to (vc)
            [obj2 opt2]
            [post (query-vc expr)])  
-       (∃-solve `(,@(pre) ,(spec-assumes post) ,(spec-asserts post)) kw1 obj1 kw2 obj2))]))
\ No newline at end of file
+       (∃-solve `(,@(pre) ,(vc-assumes post) ,(vc-asserts post)) kw1 obj1 kw2 obj2))]))
\ No newline at end of file
diff --git a/sdsl/bv/lang/core.rkt b/sdsl/bv/lang/core.rkt
index 0cb901a4..a64caf7c 100644
--- a/sdsl/bv/lang/core.rkt
+++ b/sdsl/bv/lang/core.rkt
@@ -5,7 +5,7 @@
   (only-in "program.rkt" trace* trace-args trace-out well-formed-program well-formed-trace)
   rosette/query/eval "log.rkt"
   (only-in rosette/base/core/term term? constant? get-type term-cache term<?)
-  (only-in rosette/base/core/bool ! || && => with-vc spec-assumes spec-asserts)
+  (only-in rosette/base/core/bool ! || && => with-vc vc-assumes vc-asserts)
   (only-in rosette/base/core/result result-state)
   (only-in rosette/base/core/real @integer?)
   (only-in rosette/base/core/bitvector bitvector bitvector-size)
@@ -93,8 +93,8 @@
             [(unsat? cex) candidate]
             [else (loop (guess cex))]))])))
 
-(define (normal? sp) (list (spec-assumes sp) (spec-asserts sp)))
-(define (crash? sp)  (list (spec-assumes sp) (! (spec-asserts sp))))
+(define (normal? sp) (list (vc-assumes sp) (vc-asserts sp)))
+(define (crash? sp)  (list (vc-assumes sp) (! (vc-asserts sp))))
 
 (define (φ_synth trace spec) ;(printf "φ_synth: ~a\n" trace)
   `(,@(normal? (φ_wft trace)) ,@(normal? (φ_spec trace spec))))
diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt
index 057559ce..fd0dd8ed 100644
--- a/test/base/bitvector.rkt
+++ b/test/base/bitvector.rkt
@@ -406,9 +406,9 @@
          [v expected-value]
          [a (apply && expected-asserts)])
     (check-equal? (result-value r) v)
-    (check-equal? (spec-assumes (result-state r)) #t)
-    (or (equal? (spec-asserts (result-state r)) a)
-        (check-pred unsat? (solve (! (<=> (spec-asserts (result-state r)) a)))))))
+    (check-equal? (vc-assumes (result-state r)) #t)
+    (or (equal? (vc-asserts (result-state r)) a)
+        (check-pred unsat? (solve (! (<=> (vc-asserts (result-state r)) a)))))))
 
 (define-syntax check-bv-exn
   (syntax-rules ()
diff --git a/test/base/bvlib.rkt b/test/base/bvlib.rkt
index a7fce973..efafb3d4 100644
--- a/test/base/bvlib.rkt
+++ b/test/base/bvlib.rkt
@@ -2,7 +2,7 @@
 
 (require rackunit rackunit/text-ui (rename-in rackunit [check-exn rackunit/check-exn])
          rosette/lib/roseunit (only-in rosette/base/core/merge merge*))
-(require (only-in rosette/base/core/bool spec-assumes spec-asserts) )
+(require (only-in rosette/base/core/bool vc-assumes vc-asserts) )
 
 (define-symbolic z (bitvector 1))
 (define-symbolic x u (bitvector 4))
@@ -19,13 +19,13 @@
   (let ([ra (with-vc actual)]
         [re (with-vc expected)])
     (check-pred unsat?
-                (verify (assert (equal? (spec-assumes (result-state ra))
-                                        (spec-assumes (result-state re))))))
+                (verify (assert (equal? (vc-assumes (result-state ra))
+                                        (vc-assumes (result-state re))))))
     (check-pred unsat?
-                (verify (assert (equal? (spec-asserts (result-state ra))
-                                        (spec-asserts (result-state re))))))
+                (verify (assert (equal? (vc-asserts (result-state ra))
+                                        (vc-asserts (result-state re))))))
     (check-pred unsat?
-                (verify (begin (assume (&& (spec-assumes (result-state ra)) (spec-asserts (result-state ra))))
+                (verify (begin (assume (&& (vc-assumes (result-state ra)) (vc-asserts (result-state ra))))
                                (assert (equal? (result-value ra) (result-value re))))))))
 
 
diff --git a/test/base/eval-guarded.rkt b/test/base/eval-guarded.rkt
index ba5e1217..fae8d4ce 100644
--- a/test/base/eval-guarded.rkt
+++ b/test/base/eval-guarded.rkt
@@ -12,12 +12,12 @@
                   vc vc-clear! with-vc vc-merge!
                   $assume $assert @assume @assert
                   vc-true vc-true?
-                  spec-assumes spec-asserts)
+                  vc-assumes vc-asserts)
          (only-in rosette/base/core/real @integer? @= @<)
          (only-in rosette/base/core/merge merge merge*))
 
-(define (spec-eqv? actual assumes asserts)
-  (unsat? (solve (! (&&  (<=> (spec-assumes actual) assumes) (<=> (spec-asserts actual) asserts))))))
+(define (vc-eqv? actual assumes asserts)
+  (unsat? (solve (! (&&  (<=> (vc-assumes actual) assumes) (<=> (vc-asserts actual) asserts))))))
 
 (define (int-eqv? actual expected)
   (unsat? (solve (! (@= actual expected)))))
@@ -27,13 +27,13 @@
     (match-define (ans (ans v st) sp) actual)
     (check-equal? v e-val)
     (check-store st e-store)
-    (check-true (spec-eqv? sp e-assumes e-asserts))))
+    (check-true (vc-eqv? sp e-assumes e-asserts))))
 
 (define-syntax-rule (check-halt actual e-exn? e-assumes e-asserts)
   (begin
     (match-define (halt ex sp) actual)
     (check-pred e-exn? ex) 
-    (check-true (spec-eqv? sp e-assumes e-asserts))))
+    (check-true (vc-eqv? sp e-assumes e-asserts))))
 
 (define (check-eval-assuming)
   (define-symbolic g a b @boolean?)
diff --git a/test/base/finitize.rkt b/test/base/finitize.rkt
index 4973b3ab..8b8a9acd 100644
--- a/test/base/finitize.rkt
+++ b/test/base/finitize.rkt
@@ -35,7 +35,7 @@
 
 (define-syntax-rule (finitize/solve bw constraint ...)
   (let* ([terms (result-state (with-vc (begin (@assert constraint) ...)))]
-         [terms (list (spec-assumes terms) (spec-asserts terms))]
+         [terms (list (vc-assumes terms) (vc-asserts terms))]
          [fmap (finitize terms bw)]
          [fsol (apply solve (map (curry hash-ref fmap) terms))])
     (lift-solution fsol fmap)))
diff --git a/test/base/real.rkt b/test/base/real.rkt
index d7915d90..c0f420c1 100644
--- a/test/base/real.rkt
+++ b/test/base/real.rkt
@@ -25,8 +25,8 @@
     (match (with-vc (type-cast type val))
       [(and r (or (ans v sp) (halt v sp)))
        (when (ans? r) (check-equal? v out))
-       (check-equal? (spec-assumes sp) #t)
-       (check-equal? (spec-asserts sp) accepted?)]))
+       (check-equal? (vc-assumes sp) #t)
+       (check-equal? (vc-asserts sp) accepted?)]))
 
 (define-syntax check-valid?
   (syntax-rules ()
@@ -35,7 +35,7 @@
     [(_ (op e ...) expected [pred? ...])
      (let ([actual (op e ...)])
       (check-equal? actual expected) 
-      (define preconditions (&& (spec-assumes (vc)) (spec-asserts (vc))))
+      (define preconditions (&& (vc-assumes (vc)) (vc-asserts (vc))))
       (vc-clear!)
       (define pred (lambda (x) (or (pred? x) ...)))
       (check-pred pred (solve (! (@equal? (expression op e ...) expected)) preconditions)))]))
@@ -43,7 +43,7 @@
 (define-syntax-rule (test-valid? ([var sym] ...) (op e ...) expected)
   (let ([actual (op e ...)])
     (check-equal? actual expected)
-    (define preconditions (&& (spec-assumes (vc)) (spec-asserts (vc))))
+    (define preconditions (&& (vc-assumes (vc)) (vc-asserts (vc))))
     (vc-clear!)
     (for* ([var (in-range minval maxval+1)] ...)
       (define sol (sat (make-immutable-hash (list (cons sym var) ...))))
@@ -97,8 +97,8 @@
 (define-syntax-rule (check-state actual expected-value expected-asserts)
   (let ([r (with-vc actual)])
     (check-equal? (result-value r) expected-value)
-    (check-equal? (spec-assumes (result-state r)) #t)
-    (check-equal? (spec-asserts (result-state r)) (apply && expected-asserts))))
+    (check-equal? (vc-assumes (result-state r)) #t)
+    (check-equal? (vc-asserts (result-state r)) (apply && expected-asserts))))
 
 (define (check-real?)
   (check-equal? (@real? 1) #t)
diff --git a/test/base/vc.rkt b/test/base/vc.rkt
index a83c0688..958f46de 100644
--- a/test/base/vc.rkt
+++ b/test/base/vc.rkt
@@ -9,7 +9,7 @@
                   vc vc-clear! with-vc vc-merge!
                   $assume $assert @assume @assert
                   vc-true vc-true?
-                  spec-assumes spec-asserts)
+                  vc-assumes vc-asserts)
          (only-in rosette/base/core/real @integer? @=)
          (only-in rosette/base/core/merge merge merge*))
 
@@ -17,7 +17,7 @@
 
 (define (check-vc-eqv assumes asserts)
   (define actual (vc))
-  (check-unsat (solve (! (&&  (<=> (spec-assumes actual) assumes) (<=> (spec-asserts actual) asserts))))))
+  (check-unsat (solve (! (&&  (<=> (vc-assumes actual) assumes) (<=> (vc-asserts actual) asserts))))))
 
 (define-syntax (check-exn-svm stx)
   (syntax-case stx ()
@@ -29,13 +29,13 @@
                (regexp-match rx (exn-message ex))))
         thunk)]))
 
-(define-syntax-rule (check-assume-or-assert $a @a user? core? spec-a spec-other)
+(define-syntax-rule (check-assume-or-assert $a @a user? core? vc-a vc-other)
   (begin
     ;---------------------------;
     (define (check-vc expected-a expected-other)
       (define actual (vc))
-      (check-equal? (spec-a actual) expected-a)
-      (check-equal? (spec-other actual) expected-other))
+      (check-equal? (vc-a actual) expected-a)
+      (check-equal? (vc-other actual) expected-other))
     ;---------------------------;
     ($a #t)
     (check-pred vc-true? (vc))
@@ -82,13 +82,13 @@
 
 (define (check-assumes)
    (check-assume-or-assert $assume @assume exn:fail:svm:assume:user? exn:fail:svm:assume:core?
-                           spec-assumes spec-asserts))
+                           vc-assumes vc-asserts))
 
 (define (check-asserts)
    (check-assume-or-assert $assert @assert exn:fail:svm:assert:user? exn:fail:svm:assert:core?
-                           spec-asserts spec-assumes))
+                           vc-asserts vc-assumes))
 
-(define (spec->pair s) (cons (spec-assumes s) (spec-asserts s)))
+(define (vc->pair s) (cons (vc-assumes s) (vc-asserts s)))
 
 
 (define (check-with-vc-0)
@@ -96,71 +96,71 @@
   ;---------------------------;
   (check-match (with-vc (@assume 1)) (ans (? void?) (? vc-true?)))
   (check-pred vc-true? (vc))
-  (check-match (with-vc (@assume a)) (ans (? void?) (app spec->pair (cons (== a) #t))))
+  (check-match (with-vc (@assume a)) (ans (? void?) (app vc->pair (cons (== a) #t))))
   (check-pred vc-true? (vc))
-  (check-match (with-vc (@assume #f)) (halt (? exn:fail:svm:assume:user?) (app spec->pair (cons #f #t))))
-  (check-match (with-vc ($assume #f)) (halt (? exn:fail:svm:assume:core?) (app spec->pair (cons #f #t))))
+  (check-match (with-vc (@assume #f)) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc ($assume #f)) (halt (? exn:fail:svm:assume:core?) (app vc->pair (cons #f #t))))
   ;---------------------------;
   (check-match (with-vc (@assert 1)) (ans (? void?) (? vc-true?)))
   (check-pred vc-true? (vc))
-  (check-match (with-vc (@assert a)) (ans (? void?) (app spec->pair (cons #t (== a)))))
+  (check-match (with-vc (@assert a)) (ans (? void?) (app vc->pair (cons #t (== a)))))
   (check-pred vc-true? (vc))
-  (check-match (with-vc (@assert #f)) (halt (? exn:fail:svm:assert:user?) (app spec->pair (cons #t #f))))
-  (check-match (with-vc ($assert #f)) (halt (? exn:fail:svm:assert:core?) (app spec->pair (cons #t #f))))
-  (check-match (with-vc (1)) (halt (? exn:fail:svm:assert:err?) (app spec->pair (cons #t #f)))))
+  (check-match (with-vc (@assert #f)) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc ($assert #f)) (halt (? exn:fail:svm:assert:core?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (1)) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons #t #f)))))
 
 (define (check-with-vc-1)
   (define-symbolic a b c d @boolean?)
   ;---------------------------;
-  (check-match (with-vc (begin (@assume a) (@assume b))) (ans (? void?) (app spec->pair (cons (== (&& a b)) #t))))
-  (check-match (with-vc (begin (@assert a) (@assert b))) (ans (? void?) (app spec->pair (cons #t (== (&& a b))))))
-  (check-match (with-vc (begin (@assume a) (@assert b))) (ans (? void?) (app spec->pair (cons (== a) (== (=> a b))))))
-  (check-match (with-vc (begin (@assert a) (@assume b))) (ans (? void?) (app spec->pair (cons (== (=> a b)) (== a)))))
+  (check-match (with-vc (begin (@assume a) (@assume b))) (ans (? void?) (app vc->pair (cons (== (&& a b)) #t))))
+  (check-match (with-vc (begin (@assert a) (@assert b))) (ans (? void?) (app vc->pair (cons #t (== (&& a b))))))
+  (check-match (with-vc (begin (@assume a) (@assert b))) (ans (? void?) (app vc->pair (cons (== a) (== (=> a b))))))
+  (check-match (with-vc (begin (@assert a) (@assume b))) (ans (? void?) (app vc->pair (cons (== (=> a b)) (== a)))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assume a) (@assume (! a)))) (halt (? exn:fail:svm:assume:user?) (app spec->pair (cons #f #t))))
-  (check-match (with-vc (begin ($assume a) (@assume (! a)))) (halt (? exn:fail:svm:assume:user?) (app spec->pair (cons #f #t))))
-  (check-match (with-vc (begin (@assume (! a)) ($assume a))) (halt (? exn:fail:svm:assume:core?) (app spec->pair (cons #f #t))))
-  (check-match (with-vc (begin ($assume (! a)) ($assume a))) (halt (? exn:fail:svm:assume:core?) (app spec->pair (cons #f #t))))
+  (check-match (with-vc (begin (@assume a) (@assume (! a)))) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (begin ($assume a) (@assume (! a)))) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (begin (@assume (! a)) ($assume a))) (halt (? exn:fail:svm:assume:core?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (begin ($assume (! a)) ($assume a))) (halt (? exn:fail:svm:assume:core?) (app vc->pair (cons #f #t))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assert a) (@assert (! a)))) (halt (? exn:fail:svm:assert:user?) (app spec->pair (cons #t #f))))
-  (check-match (with-vc (begin ($assert a) (@assert (! a)))) (halt (? exn:fail:svm:assert:user?) (app spec->pair (cons #t #f))))
-  (check-match (with-vc (begin (@assert (! a)) ($assert a))) (halt (? exn:fail:svm:assert:core?) (app spec->pair (cons #t #f))))
-  (check-match (with-vc (begin ($assert (! a)) ($assert a))) (halt (? exn:fail:svm:assert:core?) (app spec->pair (cons #t #f))))
-  (check-match (with-vc (begin (@assert a) (1))) (halt (? exn:fail:svm:assert:err?) (app spec->pair (cons #t #f))))
+  (check-match (with-vc (begin (@assert a) (@assert (! a)))) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin ($assert a) (@assert (! a)))) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin (@assert (! a)) ($assert a))) (halt (? exn:fail:svm:assert:core?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin ($assert (! a)) ($assert a))) (halt (? exn:fail:svm:assert:core?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin (@assert a) (1))) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons #t #f))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assume a) (@assert #f))) (halt (? exn:fail:svm:assert:user?) (app spec->pair (cons (== a) (== (! a))))))
-  (check-match (with-vc (begin (@assume a) ($assert #f))) (halt (? exn:fail:svm:assert:core?) (app spec->pair (cons (== a) (== (! a))))))
-  (check-match (with-vc (begin (@assume a) (1))) (halt (? exn:fail:svm:assert:err?) (app spec->pair (cons (== a) (== (! a))))))
+  (check-match (with-vc (begin (@assume a) (@assert #f))) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons (== a) (== (! a))))))
+  (check-match (with-vc (begin (@assume a) ($assert #f))) (halt (? exn:fail:svm:assert:core?) (app vc->pair (cons (== a) (== (! a))))))
+  (check-match (with-vc (begin (@assume a) (1))) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons (== a) (== (! a))))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assert a) (@assume #f))) (halt (? exn:fail:svm:assume:user?) (app spec->pair (cons (== (! a)) (== a)))))
-  (check-match (with-vc (begin (@assert a) ($assume #f))) (halt (? exn:fail:svm:assume:core?) (app spec->pair (cons (== (! a)) (== a)))))
+  (check-match (with-vc (begin (@assert a) (@assume #f))) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons (== (! a)) (== a)))))
+  (check-match (with-vc (begin (@assert a) ($assume #f))) (halt (? exn:fail:svm:assume:core?) (app vc->pair (cons (== (! a)) (== a)))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assume #f) (@assert a))) (halt (? exn:fail:svm:assume:user?) (app spec->pair (cons #f #t))))
-  (check-match (with-vc (begin (@assert #f) (@assume a))) (halt (? exn:fail:svm:assert:user?) (app spec->pair (cons #t #f))))
-  (check-match (with-vc (begin (1) (@assume a))) (halt (? exn:fail:svm:assert:err?) (app spec->pair (cons #t #f))))
+  (check-match (with-vc (begin (@assume #f) (@assert a))) (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons #f #t))))
+  (check-match (with-vc (begin (@assert #f) (@assume a))) (halt (? exn:fail:svm:assert:user?) (app vc->pair (cons #t #f))))
+  (check-match (with-vc (begin (1) (@assume a))) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons #t #f))))
   ;---------------------------;
-  (check-match (with-vc (begin (@assume a) (1) (@assert b))) (halt (? exn:fail:svm:assert:err?) (app spec->pair (cons (== a) (== (! a))))))
+  (check-match (with-vc (begin (@assume a) (1) (@assert b))) (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons (== a) (== (! a))))))
   ;---------------------------;
   (check-match (with-vc (begin (@assume a) (@assume b) (@assert c) (@assert d)))
-               (ans (? void?) (app spec->pair (cons (== (&& a b)) (== (&& (=> (&& a b) c) (=> (&& a b) d)))))))
+               (ans (? void?) (app vc->pair (cons (== (&& a b)) (== (&& (=> (&& a b) c) (=> (&& a b) d)))))))
   (check-match (with-vc (begin (@assert a) (@assert b) (@assume c) (@assume d)))
-               (ans (? void?) (app spec->pair (cons (== (&& (=> (&& a b) c) (=> (&& a b) d))) (== (&& a b))))))
+               (ans (? void?) (app vc->pair (cons (== (&& (=> (&& a b) c) (=> (&& a b) d))) (== (&& a b))))))
   (check-match (with-vc (begin (@assume a) (@assert b) (@assume c) (@assert d)))
-               (ans (? void?) (app spec->pair (cons (== (&& a (=> (=> a b) c))) (== (&& (=> a b) (=> (&& a (=> (=> a b) c)) d)))))))
+               (ans (? void?) (app vc->pair (cons (== (&& a (=> (=> a b) c))) (== (&& (=> a b) (=> (&& a (=> (=> a b) c)) d)))))))
   (check-match (with-vc (begin (@assert a) (@assume b) (@assert c) (@assume d)))
-               (ans (? void?) (app spec->pair (cons (== (&& (=> a b) (=> (&& a (=> (=> a b) c)) d))) (== (&& a (=> (=> a b) c)))))))
+               (ans (? void?) (app vc->pair (cons (== (&& (=> a b) (=> (&& a (=> (=> a b) c)) d))) (== (&& a (=> (=> a b) c)))))))
   ;---------------------------;
   (check-match (with-vc (begin (@assume a) (@assert b) (@assume #f) (@assert d)))
-               (halt (? exn:fail:svm:assume:user?) (app spec->pair (cons (== (&& a (=> (=> a b) #f))) (== (=> a b))))))
+               (halt (? exn:fail:svm:assume:user?) (app vc->pair (cons (== (&& a (=> (=> a b) #f))) (== (=> a b))))))
   (check-match (with-vc (begin (@assume a) (@assert b) (1) (@assert d)))
-               (halt (? exn:fail:svm:assert:err?) (app spec->pair (cons (== a) (== (&& (=> a b) (=> a #f)))))))
+               (halt (? exn:fail:svm:assert:err?) (app vc->pair (cons (== a) (== (&& (=> a b) (=> a #f)))))))
   ;---------------------------;
   (@assume a)
   (@assert b)
-  (check-match (vc) (app spec->pair (cons (== a) (== (=> a b)))))
+  (check-match (vc) (app vc->pair (cons (== a) (== (=> a b)))))
   (check-match (with-vc (begin  (@assume c) (@assert d)))
-               (ans (? void?) (app spec->pair (cons (== (&& a (=> (=> a b) c))) (== (&& (=> a b) (=> (&& a (=> (=> a b) c)) d)))))))
-  (check-match (vc) (app spec->pair (cons (== a) (== (=> a b)))))
+               (ans (? void?) (app vc->pair (cons (== (&& a (=> (=> a b) c))) (== (&& (=> a b) (=> (&& a (=> (=> a b) c)) d)))))))
+  (check-match (vc) (app vc->pair (cons (== a) (== (=> a b)))))
   (vc-clear!))
   
   
@@ -172,10 +172,10 @@
   ;---------------------------;
   (match-define (ans _ vc0) (with-vc (begin (@assume a) (@assert b))))
   (vc-merge! (list #t) (list vc0))
-  (check-match (vc) (app spec->pair (cons (== a) (== (=> a b)))))
+  (check-match (vc) (app vc->pair (cons (== a) (== (=> a b)))))
   (vc-clear!)
   (vc-merge! (list c) (list vc0))
-  (check-match (vc) (app spec->pair (cons (== (=> c a)) (== (=> c (=> a b))))))
+  (check-match (vc) (app vc->pair (cons (== (=> c a)) (== (=> c (=> a b))))))
   (vc-clear!)
   (vc-merge! (list #f) (list vc0))
   (check-pred vc-true? (vc))
@@ -184,7 +184,7 @@
   (vc-merge! (list #f) (list vc1))
   (check-pred vc-true? (vc))
   (vc-merge! (list c) (list vc1))
-  (check-match (vc) (app spec->pair (cons (== (=> c #f)) #t)))
+  (check-match (vc) (app vc->pair (cons (== (=> c #f)) #t)))
   (check-exn-svm exn:fail:svm:assume:core? #rx"contradiction" (thunk (vc-merge! (list #t) (list vc1))))
   (vc-clear!)
   ;---------------------------;
@@ -192,20 +192,20 @@
   (vc-merge! (list #f) (list vc2))
   (check-pred vc-true? (vc))
   (vc-merge! (list c) (list vc2))
-  (check-match (vc) (app spec->pair (cons #t (==  (=> c #f)))))
+  (check-match (vc) (app vc->pair (cons #t (==  (=> c #f)))))
   (check-exn-svm exn:fail:svm:assert:core? #rx"contradiction" (thunk (vc-merge! (list #t) (list vc2))))
   (vc-clear!)
   ;---------------------------;
   (@assume a)
   (match-define (ans _ vc3) (with-vc vc-true (@assume (! a))))
   (check-exn-svm exn:fail:svm:assume:core? #rx"contradiction" (thunk (vc-merge! (list #t) (list vc3))))
-  (check-match (vc) (app spec->pair (cons #f #t)))
+  (check-match (vc) (app vc->pair (cons #f #t)))
   (vc-clear!)
   ;---------------------------;
   (@assert a)
   (match-define (ans _ vc4) (with-vc vc-true (@assert (! a))))
   (check-exn-svm exn:fail:svm:assert:core? #rx"contradiction" (thunk (vc-merge! (list #t) (list vc4))))
-  (check-match (vc) (app spec->pair (cons #t #f)))
+  (check-match (vc) (app vc->pair (cons #t #f)))
   (vc-clear!))
 
 (define (check-vc-merge-1)
@@ -215,16 +215,16 @@
   (check-pred vc-true? (vc))
   ;---------------------------;
   (vc-merge! (list a not-a) (list (result-state (with-vc (@assume b))) (result-state (with-vc (@assume c)))))
-  (check-match (vc) (app spec->pair (cons (== (&& (=> a b) (=> not-a c))) #t)))
+  (check-match (vc) (app vc->pair (cons (== (&& (=> a b) (=> not-a c))) #t)))
   (vc-clear!)
   (vc-merge! (list a not-a) (list (result-state (with-vc (@assert b))) (result-state (with-vc (@assert c)))))
-  (check-match (vc) (app spec->pair (cons #t (== (&& (=> a b) (=> not-a c))))))
+  (check-match (vc) (app vc->pair (cons #t (== (&& (=> a b) (=> not-a c))))))
   (vc-clear!)
   (vc-merge! (list a not-a) (list (result-state (with-vc (@assume b))) (result-state (with-vc (@assert c)))))
-  (check-match (vc) (app spec->pair (cons (== (=> a b)) (== (=> not-a c)))))
+  (check-match (vc) (app vc->pair (cons (== (=> a b)) (== (=> not-a c)))))
   (vc-clear!)
   (vc-merge! (list a not-a) (list (result-state (with-vc (@assert b))) (result-state (with-vc (@assume c)))))
-  (check-match (vc) (app spec->pair (cons (== (=> not-a c)) (== (=> a b)))))
+  (check-match (vc) (app vc->pair (cons (== (=> not-a c)) (== (=> a b)))))
   (vc-clear!)
   (@assume d)
   (@assert e)
@@ -242,18 +242,18 @@
                  (thunk (vc-merge! (list a not-a)
                                    (list (result-state (with-vc (@assume #f)))
                                          (result-state (with-vc (@assume #f)))))))
-  (check-match (vc) (app spec->pair (cons #f #t)))
+  (check-match (vc) (app vc->pair (cons #f #t)))
   (vc-clear!)
   (check-exn-svm exn:fail:svm:assert:core? #rx"contradiction"
                  (thunk (vc-merge! (list a not-a)
                                    (list (result-state (with-vc (@assert #f)))
                                          (result-state (with-vc (@assert #f)))))))
-  (check-match (vc) (app spec->pair (cons #t #f)))
+  (check-match (vc) (app vc->pair (cons #t #f)))
   (vc-clear!)
   (vc-merge! (list a not-a) (list (result-state (with-vc (@assume #f))) (result-state (with-vc (@assert #f)))))
-  (check-match (vc) (app spec->pair (cons (== not-a) (== a))))
+  (check-match (vc) (app vc->pair (cons (== not-a) (== a))))
   (vc-merge! (list a not-a) (list (result-state (with-vc (@assert #f))) (result-state (with-vc (@assume #f)))))
-  (check-match (vc) (app spec->pair (cons (== not-a) (== a))))
+  (check-match (vc) (app vc->pair (cons (== not-a) (== a))))
   (vc-clear!))
 
 (define assume-tests
diff --git a/test/cplex/solve.rkt b/test/cplex/solve.rkt
index 797386da..0ed5a9c0 100644
--- a/test/cplex/solve.rkt
+++ b/test/cplex/solve.rkt
@@ -9,7 +9,7 @@
 (define solver (cplex))
 (current-solver solver)
 
-(define (asserts) (list (spec-assumes (vc)) (spec-asserts (vc))))
+(define (asserts) (list (vc-assumes (vc)) (vc-asserts (vc))))
 
 (define basic-tests
   (test-suite+ "Solve basic tests."