diff --git a/forge/breaks.rkt b/forge/breaks.rkt
index 2b8954fd..9a666ec8 100644
--- a/forge/breaks.rkt
+++ b/forge/breaks.rkt
@@ -652,11 +652,18 @@
 
     (define (funcformula rllst quantvarlst)
         (cond
-            [(empty? (rest (rest rllst))) 
-                (let ([a (gensym)])
-                    (@all/info (@just-location-info loc) ([a (first rllst)]) (@one (funcformulajoin (cons a quantvarlst)))))]
-            [else (let ([a (gensym)])
-                    (@all/info (@just-location-info loc) ([a (first rllst)]) (funcformula (rest rllst) (cons a quantvarlst))))]))
+          [(empty? (rest (rest rllst)))
+           (let* ([var-id (gensym 'pfunc)]
+                  [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+             (@quantified-formula (@just-location-info loc) 'all
+                                  (list (cons a (first rllst)))
+                                  (@one (funcformulajoin (cons a quantvarlst)))))]
+            [else
+             (let* ([var-id (gensym 'pfunc)]
+                  [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
+             (@quantified-formula (@just-location-info loc) 'all
+                                  (list (cons a (first rllst)))
+                                  (funcformula (rest rllst) (cons a quantvarlst))))]))
     (define formulas (set (funcformula rel-list (list))))
     
     ; OLD CODE
@@ -733,17 +740,12 @@
                        (@quantified-formula (@just-location-info loc) 'all
                                             (list (cons a (first rllst)))
                                             (@lone (pfuncformulajoin (cons a quantvarlst)))))]
-                    ;(@all/info (@just-location-info loc) ([a (first rllst)])
-                    ;           (@lone (pfuncformulajoin (cons a quantvarlst)))))]
                     [else (let* ([var-id (gensym 'pfunc)]
                                  [a (@node/expr/quantifier-var (@just-location-info loc) 1 var-id var-id)])
-                            ;(@all/info (@just-location-info loc) ([a (first rllst)])
-                            ;           (pfuncformula (rest rllst) (cons a quantvarlst))
                             (@quantified-formula (@just-location-info loc) 'all
                                                  (list (cons a (first rllst)))
                                                  (pfuncformula (rest rllst) (cons a quantvarlst))))]))
                 (define pf-fmla (pfuncformula rel-list (list)))
-                (printf "pfunc breaker: ~a~n" pf-fmla)
                 (define formulas (set pf-fmla))
                 
     ; OLD CODE
diff --git a/forge/lang/expander.rkt b/forge/lang/expander.rkt
index 7b4f638c..b43d4501 100644
--- a/forge/lang/expander.rkt
+++ b/forge/lang/expander.rkt
@@ -54,7 +54,7 @@
 
 (define-for-syntax (my-expand stx)
   (define core-funcs-and-macros
-    (map (curry datum->syntax stx)
+    (map (lambda (s) (datum->syntax stx s stx))
          '(^ * ~ + - & join
            -> => implies ! not and or && || ifte iff <=>
            = in ni != !in !ni is
@@ -159,14 +159,14 @@
     (pattern ((~datum SigExt)
               "extends"
               name:QualNameClass)
-      #:attr symbol #'#:extends
-      #:attr value #'name.name)
+      #:attr symbol (syntax/loc this-syntax #:extends)
+      #:attr value (syntax/loc this-syntax name.name))
     (pattern ((~datum SigExt)
               "in" 
               name:QualNameClass
               (~seq (~seq "+" names:QualNameClass) ...))
-      #:attr symbol #'#:in
-      #:attr value #'(raise "Extending with in not yet implemented.")))
+      #:attr symbol (syntax/loc this-syntax #:in)
+      #:attr value (syntax/loc this-syntax (raise "Extending with in not yet implemented."))))
 
   ; Mult : LONE-TOK | SOME-TOK | ONE-TOK | TWO-TOK
   (define-syntax-class MultClass
@@ -209,8 +209,8 @@
                                                #'(if (> (node/expr-arity expr) 1)
                                                      'set
                                                      'one))]) 
-                         #'((names-c.names expr mult) ...))
-      #:attr names #'(names-c.names ...)))
+                         (syntax/loc this-syntax ((names-c.names expr mult) ...)))
+      #:attr names (syntax/loc this-syntax (names-c.names ...))))
   
   ; Declaration of a comma-delimited list of variable declarations with expr and optional multiplicity
   ; DeclList : Decl
@@ -531,7 +531,8 @@
               (~optional "exactly")
               name:QualNameClass)
       #:attr translate (begin (datum->syntax #'name
-                                      (list #'name.name)))))
+                                             (list #'name.name)
+                                             #'name))))
 
   (define-syntax-class QualNameOrAtomOrAtomizedNumberClass
      #:description "name, atom name, or number"
@@ -685,7 +686,9 @@
               (~and op
                     (~or "in" "=" "<" ">" "<=" ">="
                          "is" "ni")))
-      #:attr symbol (datum->syntax #'op (op-symbol-to-operator (string->symbol (syntax->datum #'op))))))
+      #:attr symbol (datum->syntax #'op
+                                   (op-symbol-to-operator (string->symbol (syntax->datum #'op)))
+                                   #'op)))
 
   ; We don't overload (e.g.) <, but we don't want users to need to write (e.g.) "int<". 
   (define (op-symbol-to-operator sym)
@@ -723,7 +726,8 @@
     (pattern ((~datum Quant) (~and q (~or "all" "no" "lone"
                                             "some" "one" "two")))
       #:attr symbol (datum->syntax #'q
-                                   (string->symbol (syntax->datum #'q))))
+                                   (string->symbol (syntax->datum #'q))
+                                   #'q))
     (pattern ((~datum Quant) (~literal sum))
       #:attr symbol (syntax/loc #'q sum-quant)))
 
@@ -832,7 +836,8 @@
                 (with-syntax ([relation-name relation-name-p1]
                               [relation-types (datum->syntax relation-types 
                                                              (cons sig-name ;(syntax->datum sig-name)
-                                                                   (syntax->list relation-types)))]                          
+                                                                   (syntax->list relation-types))
+                                                             relation-types)]                          
                               [relation-mult relation-mult]
                               [is-var relation-is-var])
                       (syntax/loc relation-name-p1 (relation (#:lang (get-check-lang)) relation-name relation-types #:is relation-mult #:is-var is-var))))))))]))
@@ -870,8 +875,10 @@
                         name:NameClass
                         decls:ParaDeclsClass
                         block:BlockClass)
-   (with-syntax ([decl (datum->syntax #'name (cons (syntax->datum #'name.name)
-                                                   (syntax->list #'decls.pairs)))]
+   (with-syntax ([decl (datum->syntax #'name
+                                      (cons (syntax->datum #'name.name)
+                                            (syntax->list #'decls.pairs))
+                                      #'name)]
                  [block #'block])
      (quasisyntax/loc stx (begin
        (~? (raise (format "Prefixes not allowed: ~a" 'prefix)))
@@ -899,7 +906,8 @@
                        output-expr:ExprClass
                        body:ExprClass)
    (with-syntax ([decl (datum->syntax #'name (cons (syntax->datum #'name.name)
-                                                   (syntax->list #'decls.pairs)))]
+                                                   (syntax->list #'decls.pairs))
+                                      #'name)]
                  ; Parser "Expr" includes both expressions and formulas. Thus, disambiguate
                  ;   (e.g.) the "Expr" `one univ` into true expr and multiplicity in the expander;
                  ;   It's not the job of the `fun` macro to handle this. (Same for `pred`, etc.)
@@ -943,7 +951,8 @@
                        (~optional scope:ScopeClass)
                        (~optional bounds:BoundsClass))
    (with-syntax ([cmd-type (datum->syntax #'cmd-type
-                                         (string->symbol (syntax->datum #'cmd-type)))]
+                                          (string->symbol (syntax->datum #'cmd-type))
+                                          #'cmd-type)]
                  [name #`(~? name.name #,(make-temporary-name stx))]
                  [preds #'(~? pred.name preds)])
     #`(begin
@@ -968,7 +977,8 @@
    (with-syntax ([name #`(~? name.name #,(make-temporary-name stx))]
                  [preds #'(~? pred.name preds)]
                  [expected (datum->syntax #'expected
-                                          (string->symbol (syntax->datum #'expected)))])
+                                          (string->symbol (syntax->datum #'expected))
+                                          #'expected)])
      (syntax/loc stx
        (test name (~? (~@ #:preds [preds]))
                   (~? (~@ #:scope scope.translate))
@@ -1009,8 +1019,8 @@
     [qpd:QuantifiedPropertyDeclClass  
     ;;;#:do [(printf "QuantifiedPropertyDeclClass.PropExprs: ~a~n" (syntax->datum #'qpd.prop-exprs))]
      (with-syntax* 
-        ( [(exp-pred-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.pred-name) (syntax->datum #'qpd.pred-exprs)))]
-          [(exp-prop-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.prop-name) (syntax->datum #'qpd.prop-exprs)))]
+        ( [(exp-pred-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.pred-name) (syntax->datum #'qpd.pred-exprs)) stx)]
+          [(exp-prop-exprs ...) (datum->syntax stx (cons (syntax->datum #'qpd.prop-name) (syntax->datum #'qpd.prop-exprs)) stx)]
         
           [prop-consolidated (if (equal? (syntax->datum #'qpd.prop-exprs) '()) 
                                 (syntax/loc stx qpd.prop-name)
@@ -1245,7 +1255,7 @@
                           op)
                     expr1:ExprClass)
    (with-syntax ([expr1 (my-expand #'expr1)]
-                 [op (datum->syntax #'op (string->symbol (syntax->datum #'op)))])
+                 [op (datum->syntax #'op (string->symbol (syntax->datum #'op)) #'op)])
      (syntax/loc stx (op (#:lang (get-check-lang)) expr1)))]
 
   [((~datum Expr) "#" expr1:ExprClass)
@@ -1439,11 +1449,13 @@
      (with-syntax ([ellip '...])
        (syntax/loc stx-outer
          (define-syntax (macro-id stx)
+           ; Uncomment this if debugging loss of syntax location. Look through the spam for
+           ; syntax that doesn't carry a location or that has unexpected location.
+           ;(printf "in macro-id ~a: ~a~n" 'macro-id stx)
            (syntax-parse stx
              #:track-literals
              [((~var macro-id id) . pattern) pattern-directive ... (syntax/loc stx template)]))))]))
 
-
 (dsm-keep (Expr1 stx ...) (Expr stx ...))
 (dsm-keep (Expr2 stx ...) (Expr stx ...))
 (dsm-keep (Expr3 stx ...) (Expr stx ...))
diff --git a/forge/last-checker.rkt b/forge/last-checker.rkt
index 769dab14..c4de5b39 100644
--- a/forge/last-checker.rkt
+++ b/forge/last-checker.rkt
@@ -394,7 +394,7 @@
                                     (map (lambda (decl)
                                           (let ([var (car decl)]
                                                 [domain (cdr decl)])
-                                            (printf "!!!!! comprehension case; var: ~a; domain: ~a; quantvars: ~a~n" var domain quantvars)
+                                            ;(printf "!!!!! comprehension case; var: ~a; domain: ~a; quantvars: ~a~n" var domain quantvars)
                                             ; CHECK: shadowed variables
                                             ; It does NOT suffice to do: (assoc var quantvars), since we now give variables
                                             ; distinct gensym suffixes to help with disambiguation.
diff --git a/forge/sigs-structs.rkt b/forge/sigs-structs.rkt
index df431976..5a1cd738 100644
--- a/forge/sigs-structs.rkt
+++ b/forge/sigs-structs.rkt
@@ -662,8 +662,9 @@ Returns whether the given run resulted in sat or unsat, respectively.
      (&&/info info
               (=>/info info a b)
               (=>/info info (!/info info a) c))]
-    ; It's an expression if-then-else
-    [(and (node/expr? b) (node/expr? c))
+    ; It's an expression if-then-else (note: mixing int-expr and rel-expr is OK)
+    [(and (or (node/expr? b) (node/int? b) (integer? b))
+          (or (node/expr? c) (node/int? c) (integer? c)))
      (ite/info info a b c)]
     ; It's an error
     [else
diff --git a/forge/tests/forge/relations/breakers.frg b/forge/tests/forge/relations/breakers.frg
index 28a75d74..29214a70 100644
--- a/forge/tests/forge/relations/breakers.frg
+++ b/forge/tests/forge/relations/breakers.frg
@@ -44,11 +44,8 @@ test expect {
     -- Overlap with a previous test, but keep since it checks a valuable syntax foible
     cardinalityCheckSyntax: { {#{a: A | some FrontDesk.p[a]}} > 1} is sat
 
-    -- TODO BAD ERRORS: recording here for discussion
-    -- Run-spec: contract violation expected: node/formula? given: (Relation l)
-    --BAD_ERROR_1: {l} is sat 
     -- expander.rkt:701:40: preds: attribute contains non-syntax value    
-    --BAD_ERROR_2: {no l} is sat for {A = `A0 + `A1} is sat
+    -- BAD_ERROR_2: {no l} is sat for {A = `A0 + `A1} is sat
 
     ----- test "linear" -----