The time is now Sunday, June 15th, 2025 8:20:56pm
(/usr/bin/env PLTUSERHOME=/home/root//user PLT_PKG_BUILD_SERVICE=1 CI=true PLT_INFO_ALLOW_VARS=;PLT_PKG_BUILD_SERVICE PLTCOMPILEDROOTS=/home/root//zo: PLT_PKG_BUILD_SERVICE=1 /usr/bin/xvfb-run -n 1 /bin/sh -c cd "/home/root/"/racket && bin/racket -MCR "/home/root/"/zo: -l- raco pkg install --jobs 1 -u --auto knox && bin/racket -MCR "/home/root/"/zo: -l- raco test --jobs 1 --timeout 180 --drdr --package knox)
Resolved "knox" via file:///home/root//catalogs/built/catalog
Resolved "rosette" via file:///home/root//catalogs/built/catalog
00: Resolved "custom-load" via file:///home/root//catalogs/built/catalog
Resolved "rfc6455" via file:///home/root//catalogs/built/catalog
The following uninstalled packages were listed as dependencies
and they were automatically installed:
 dependencies of knox:
   rosette
 dependencies of rosette:
   custom-load
   rfc6455
raco setup: version: 8.17.0.4
raco setup: platform: x86_64-linux-natipkg [cs]
raco setup: target machine: any
raco setup: cross-installation: yes
raco setup: installation name: 8.17.0.4
raco setup: variants: cs
raco setup: main collects: /home/root/racket/collects/
raco setup: collects paths: 
raco setup:   /home/root/user/.local/share/racket/8.17.0.4/collects
raco setup:   /home/root/racket/collects/
raco setup: main pkgs: /home/root/racket/share/pkgs
raco setup: pkgs paths: 
raco setup:   /home/root/racket/share/pkgs
raco setup:   /home/root//user/.local/share/racket/8.17.0.4/pkgs
raco setup: links files: 
raco setup:   /home/root/racket/share/links.rktd
raco setup:   /home/root//user/.local/share/racket/8.17.0.4/links.rktd
raco setup: compiled-file roots: 
raco setup:   /home/root//zo
raco setup:   same
raco setup: --- updating info-domain tables ---                    [1:21:14]
raco setup: updating: /home/root/user/.local/share/racket/8.17.0.4/share/info-cache.rktd
raco setup: --- pre-installing collections ---                     [1:21:14]
raco setup: pre-installing: <pkgs>/rosette/rosette


********** Failed to install Z3 **********

Rosette installed successfully, but wasn't able to install the Z3 SMT solver.

You'll need to manually install a Z3 binary at this location:
    /home/root/user/.local/share/racket/8.17.0.4/pkgs/rosette/bin/z3
or anywhere that is on your PATH. Alternatively, in your programs, you can
construct a solver object manually:
    (current-solver (z3 #:path "/path/to/z3"))

Note that Rosette ships with a specific release of Z3 (v4.8.8). Installing a
different version of Z3 may change the performance of Rosette programs.

The problem was:
    tcp-connect: host not found
  hostname: github.com
  port number: 443
  system error: Temporary failure in name resolution; gai_err=-3

**********


raco setup: --- installing foreign libraries ---                   [1:21:15]
raco setup: --- installing shared files ---                        [1:21:15]
raco setup: --- compiling collections ---                          [1:21:15]
raco setup: making: <pkgs>/custom-load (custom-load)
raco setup:  in <pkgs>/custom-load
raco setup:  in <pkgs>/custom-load/private
raco setup: making: <pkgs>/custom-load/private
raco setup: making: <pkgs>/knox/knox
raco setup:  in <pkgs>/knox/knox
raco setup:  in <pkgs>/knox/rosutil
raco setup:  in <pkgs>/rosette/rosette
raco setup:  in <pkgs>/rosette/rosette/base
raco setup:  in <pkgs>/rosette/rosette/base/adt
raco setup:  in <pkgs>/rosette/rosette/base/core
raco setup:  in <pkgs>/rosette/rosette/base/form
raco setup:  in <pkgs>/rosette/rosette/base/struct
raco setup:  in <pkgs>/rosette/rosette/query
raco setup:  in <pkgs>/rosette/rosette/solver
raco setup:  in <pkgs>/rosette/rosette/solver/smt
raco setup:  in <pkgs>/knox/yosys
raco setup:  in <pkgs>/rosette/rosette/safe/lang
raco setup: making: <pkgs>/knox/knox/circuit
raco setup:  in <pkgs>/knox/knox/circuit
raco setup: making: <pkgs>/knox/knox/circuit/lang
raco setup:  in <pkgs>/knox/knox/circuit/lang
raco setup: making: <pkgs>/knox/knox/correctness
raco setup:  in <pkgs>/knox/knox/correctness
raco setup:  in <pkgs>/knox/rosutil
raco setup:  in <pkgs>/knox/knox/driver
raco setup:  in <pkgs>/knox/knox/semantics
raco setup:  in <pkgs>/rosette/rosette/lib
raco setup:  in <pkgs>/rosette/rosette
raco setup:  in <pkgs>/knox/yosys
raco setup: making: <pkgs>/knox/knox/correctness/lang
raco setup:  in <pkgs>/knox/knox/correctness/lang
raco setup: making: <pkgs>/knox/knox/driver
raco setup:  in <pkgs>/knox/knox/driver
raco setup: making: <pkgs>/knox/knox/driver/lang
raco setup:  in <pkgs>/knox/knox/driver/lang
raco setup: making: <pkgs>/knox/knox/emulator
raco setup:  in <pkgs>/knox/knox/emulator
raco setup:  in <pkgs>/knox/test/yosys/verilog
raco setup:  in <pkgs>/knox/yosys/lang
raco setup:  in <pkgs>/knox/yosys
raco setup: making: <pkgs>/knox/knox/emulator/lang
raco setup:  in <pkgs>/knox/knox/emulator/lang
raco setup: making: <pkgs>/knox/knox/security
raco setup:  in <pkgs>/knox/knox/security
raco setup: making: <pkgs>/knox/knox/security/lang
raco setup:  in <pkgs>/knox/knox/security/lang
raco setup: making: <pkgs>/knox/knox/semantics
raco setup: making: <pkgs>/knox/knox/spec
raco setup:  in <pkgs>/knox/knox/spec
raco setup: making: <pkgs>/knox/knox/spec/lang
raco setup:  in <pkgs>/knox/knox/spec/lang
raco setup: making: <pkgs>/knox/rosutil
raco setup: making: <pkgs>/knox/test
raco setup: making: <pkgs>/knox/yosys
raco setup: making: <pkgs>/knox/yosys/debug
raco setup:  in <pkgs>/knox/yosys/debug
raco setup: making: <pkgs>/knox/yosys/debug/expand
raco setup: making: <pkgs>/knox/yosys/debug/expand/lang
raco setup:  in <pkgs>/knox/yosys/debug/expand/lang
raco setup: making: <pkgs>/knox/yosys/debug/read
raco setup: making: <pkgs>/knox/yosys/debug/read/lang
raco setup:  in <pkgs>/knox/yosys/debug/read/lang
raco setup: making: <pkgs>/knox/yosys/lang
raco setup: making: <pkgs>/rfc6455/net
raco setup:  in <pkgs>/rfc6455/net
raco setup:  in <pkgs>/rfc6455/net/rfc6455
raco setup:  in <pkgs>/rfc6455/net/rfc6455/hybi00
raco setup:  in <pkgs>/rfc6455/net/rfc6455/private
raco setup:  in <pkgs>/rfc6455/net/rfc6455/rfc6455
raco setup: making: <pkgs>/rfc6455/net/rfc6455
raco setup:  in <pkgs>/rfc6455/net/rfc6455
raco setup:  in <pkgs>/rfc6455/net/rfc6455/scribblings
raco setup: making: <pkgs>/rfc6455/net/rfc6455/examples
raco setup:  in <pkgs>/rfc6455/net/rfc6455/examples
raco setup: making: <pkgs>/rfc6455/net/rfc6455/hybi00
raco setup: making: <pkgs>/rfc6455/net/rfc6455/private
raco setup: making: <pkgs>/rfc6455/net/rfc6455/rfc6455
raco setup: making: <pkgs>/rfc6455/net/rfc6455/scribblings
raco setup: making: <pkgs>/rosette/rosette
raco setup:  in <pkgs>/rosette/rosette
raco setup:  in <pkgs>/rosette/rosette/guide/scribble
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/datatypes
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/util
raco setup:  in <pkgs>/rosette/rosette/solver/smt
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/error-tracing
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/essentials
raco setup:  in <pkgs>/rosette/rosette/lib
raco setup:  in <pkgs>/rosette/rosette/lib/util
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/forms
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/libs
raco setup:  in <pkgs>/rosette/rosette/lang
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/performance
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/reflection
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/unsafe
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/welcome
raco setup: making: <pkgs>/rosette/rosette/base
raco setup: making: <pkgs>/rosette/rosette/base/adt
raco setup: making: <pkgs>/rosette/rosette/base/core
raco setup: making: <pkgs>/rosette/rosette/base/form
raco setup: making: <pkgs>/rosette/rosette/base/struct
raco setup: making: <pkgs>/rosette/rosette/guide
raco setup: making: <pkgs>/rosette/rosette/guide/scribble
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/datatypes
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/datatypes
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/error-tracing
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/error-tracing
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/essentials
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/essentials
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/util
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/forms
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/libs
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/libs
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/performance
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/performance
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/reflection
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/unsafe
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/util
raco setup:  in <pkgs>/rosette/rosette/guide/scribble/util
raco setup: making: <pkgs>/rosette/rosette/guide/scribble/welcome
raco setup: making: <pkgs>/rosette/rosette/lang
raco setup: making: <pkgs>/rosette/rosette/lib
raco setup:  in <pkgs>/rosette/rosette/lib
raco setup:  in <pkgs>/rosette/rosette/lib/profile
raco setup:  in <pkgs>/rosette/rosette/lib/profile/renderer
raco setup: making: <pkgs>/rosette/rosette/lib/profile
raco setup:  in <pkgs>/rosette/rosette/lib/profile
raco setup:  in <pkgs>/rosette/rosette/lib/profile/renderer
raco setup:  in <pkgs>/rosette/rosette/lib/profile/renderer/report
raco setup:  in <pkgs>/rosette/rosette/lib/util
raco setup: making: <pkgs>/rosette/rosette/lib/profile/renderer
raco setup: making: <pkgs>/rosette/rosette/lib/profile/renderer/report
raco setup: making: <pkgs>/rosette/rosette/lib/profile/renderer/report/html
raco setup: making: <pkgs>/rosette/rosette/lib/profile/renderer/report/html/css
raco setup: making: <pkgs>/rosette/rosette/lib/profile/renderer/report/html/js
raco setup: making: <pkgs>/rosette/rosette/lib/trace
raco setup:  in <pkgs>/rosette/rosette/lib/trace
raco setup: making: <pkgs>/rosette/rosette/lib/trace/report
raco setup:  in <pkgs>/rosette/rosette/lib/trace/report
raco setup: making: <pkgs>/rosette/rosette/lib/trace/report/dist
raco setup: making: <pkgs>/rosette/rosette/lib/util
raco setup: making: <pkgs>/rosette/rosette/private
raco setup: making: <pkgs>/rosette/rosette/query
raco setup: making: <pkgs>/rosette/rosette/safe
raco setup: making: <pkgs>/rosette/rosette/safe/lang
raco setup: making: <pkgs>/rosette/rosette/solver
raco setup: making: <pkgs>/rosette/rosette/solver/smt
raco setup: making: <pkgs>/rosette/sdsl
raco setup: making: <pkgs>/rosette/test
raco setup: --- creating launchers ---                             [1:22:35]
raco setup: --- installing man pages ---                           [1:22:35]
raco setup: --- building documentation ---                         [1:22:35]
raco setup: syncing: <pkgs>/custom-load/doc/custom-load
raco setup: running: <pkgs>/racket-index/scribblings/main/user/local-redirect.scrbl
raco setup: running: <pkgs>/racket-index/scribblings/main/user/release.scrbl
raco setup: syncing: <pkgs>/rfc6455/net/rfc6455/doc/rfc6455
raco setup: syncing: <pkgs>/rosette/rosette/doc/rosette-guide
raco setup: running: <pkgs>/racket-index/scribblings/main/user/search.scrbl
raco setup: running: <pkgs>/racket-index/scribblings/main/user/start.scrbl
raco setup: rendering: <pkgs>/racket-index/scribblings/main/user/local-redirect.scrbl
raco setup: rendering: <pkgs>/racket-index/scribblings/main/user/release.scrbl
raco setup: rendering: <pkgs>/racket-index/scribblings/main/user/search.scrbl
raco setup: rendering: <pkgs>/racket-index/scribblings/main/user/start.scrbl
raco setup: --- installing collections ---                         [1:22:59]
raco setup: --- post-installing collections ---                    [1:22:59]
raco setup: post-installing: <pkgs>/rosette/rosette


********** Failed to install Z3 **********

Rosette installed successfully, but wasn't able to install the Z3 SMT solver.

You'll need to manually install a Z3 binary at this location:
    /home/root/user/.local/share/racket/8.17.0.4/pkgs/rosette/bin/z3
or anywhere that is on your PATH. Alternatively, in your programs, you can
construct a solver object manually:
    (current-solver (z3 #:path "/path/to/z3"))

Note that Rosette ships with a specific release of Z3 (v4.8.8). Installing a
different version of Z3 may change the performance of Rosette programs.

The problem was:
    tcp-connect: host not found
  hostname: github.com
  port number: 443
  system error: Temporary failure in name resolution; gai_err=-3

**********


raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/info.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/circuit/circuit-lang.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/circuit/lang/reader.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/circuit.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/checker.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/correctness-lang.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/correctness.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/hint.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/lang/reader.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver/driver-lang.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver/interpreter.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver/lang/reader.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver/lib.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator/emulator-lang.rkt")
raco test: (submod (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator/interpreter.rkt") test)
interpreter.rkt: racket test: #<<non-empty stderr
--------------------
circuit
ERROR
name:       check-equal?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator/interpreter.rkt:316:4

read-solution: unrecognized solver output: #<eof>
--------------------

non-empty stderr
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator/lang/reader.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator/util.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/result.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/security/checker.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/security/lang/reader.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/security/security-lang.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/environment.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/lifted.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/shared.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/syntax.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/value.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/spec/lang/reader.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/spec/spec-lang.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/spec.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/addressable-struct.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/concretize.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/convenience.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/dependence.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/lens.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/main.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/overapproximate.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/serialization.rkt")
raco test: (submod (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/substitution.rkt") test)
raco test: (submod (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt") test)
subsumption.rkt: racket test: #<<non-empty stderr
--------------------
subsumed?: mismatched shapes but empty
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:713:4
params:     '(#t #f (1 2) #f (1) #t)

error writing to stream port
  system error: Broken pipe; errno=32
--------------------
--------------------
subsumed?: input-sensitive
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:719:4
params:
  (list #f (seteq) (mod (bv #x01 8) x$64 y$65) #t (mod (bv #x01 8) y$65 x$64) #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: mismatched shapes or definitely not equal
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:726:4
params:     '(#f #f (3) #t 3 #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: abstract
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:731:4
params:     (list #t (seteq x$68 y$69) (mod #f #f x$68) #t (mod #f #f y$69) #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: basic math
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:737:4
params:
  (list
 #t
 (seteq x$70)
 (mod #f #f x$70)
 #t
 (mod #f #f (bvadd (bv #x00000001 32) x$70))
 #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: entanglement
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:744:4
params:
  (list #f (seteq x$71 y$72) (mod #f x$71 y$72) #t (mod #f x$71 x$71) #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed? can't skip conditions
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:754:4
params:     (list #f #f x$73 (= 0 y$74) y$74 (= 0 y$74))

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: conditions
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:760:4
params:     (list #t #f (list x$75 y$76) #t (list (+ 1 x$75) y$76) #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: conditions not overlapping with fields
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:781:4
params:
  (list #f #f (list y$78) (! (= 0 (remainder x$77 2))) (list y$78) #f)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: nested structs
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:819:4
params:
  (list
 #t
 #f
 (system-state
  (ckt secret$79 (bvadd (bv #x0000000000000003 64) pc1$80) mem1$82)
  (sim-state
   spec$84
   (aux-state
    (ckt (bv #x00000000 32) (bvadd (bv #x0000000000000004 64) pc2$81) mem2$83)
    '(1 2 3 4))))
 (= spec$84 (bitvector->natural secret$79))
 (system-state
  (ckt secret$79 pc1$80 mem1$82)
  (sim-state
   spec$84
   (aux-state (ckt (bv #x00000000 32) pc2$81 mem2$83) (list 1 2 fresh$85 4))))
 (= spec$84 (bitvector->natural secret$79)))

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: case-split-merge
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:924:4
params:
  (list
 #f
 (seteq)
 (vector a$86 (bv #x00 8) (bv #x00 8))
 (bveq (bv #x00 8) x$87)
 (vector
  (ite (bveq (bv #x00 8) x$87) a$86 (bv #x00 8))
  (ite (bveq (bv #x01 8) x$87) a$86 (bv #x00 8))
  fresh$88)
 (bvult x$87 (bv #x02 8)))

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: union, basic
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:939:4
params:     '(#t #f (1 2) #t (union [b$91 (x$89)] [(! b$91) (x$89 y$90)]) #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: union, more complex
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:948:4
params:
  (list #t #f (list x$94) #t (union [b$92 x$94] [(! b$92) (x$94)]) #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: union, nested
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:977:4
params:
  '(#t
  #f
  (union [b**$98 (x$99)] [(! b**$98) #((union #:size 2 #:hash 828191789630775088))])
  #t
  (union [b**$98 (x$99)] [(! b**$98) #((union #:size 3 #:hash 781851029116874748))])
  #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed?: union, guards
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:985:4
params:
  '(#t
  #f
  (union [b$101 x$102] [(! b$101) (x$102)])
  #t
  (union [b$101 (x$102)] [(! b$101) x$102])
  #t)

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
subsumed? union, with some concrete values
ERROR
name:       check-subsumed
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt:997:4
params:
  '(#t
  #f
  (union [b$104 b$104] [(! b$104) 3])
  #t
  (union [b$104 b$104] [(! b$104) x$106])
  #t)

read-solution: unrecognized solver output: #<eof>
--------------------

non-empty stderr
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/util.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/info.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/knox/circuit/use_persistent_reset.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/knox/circuit.rkt")
circuit.rkt: racket test: #<<non-empty stderr
--------------------
crash+power-on-reset syncs persistent state before reset
ERROR
name:       check-pred
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/knox/circuit.rkt:11:2

error writing to stream port
  system error: Broken pipe; errno=32
--------------------

non-empty stderr
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/knox/driver/interpreter.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/addressable-struct.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt")
concretize.rkt: racket test: #<<non-empty stderr
--------------------
concretize: basic
ERROR
name:       check-eq?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt:15:2

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
concretize: larger
ERROR
name:       check-eq?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt:25:2

error writing to stream port
  system error: Broken pipe; errno=32
--------------------
--------------------
concretize: failure
ERROR
name:       check-equal?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt:32:2

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
concretize: non-useful predicate
ERROR
name:       check-equal?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt:38:2

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
concretize: predicate
ERROR
name:       check-equal?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt:44:2

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
concrete
ERROR
name:       check-pred
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt:50:2

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
concretize: fields subset
ERROR

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
concretize: fields all
ERROR

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
concretize: cooperation with lens-transform
ERROR
name:       check-equal?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt:76:2

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
all-values
ERROR

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
all-values limit
ERROR
name:       check-equal?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt:95:2

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
all-values predicate
ERROR
name:       check-equal?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt:100:2

read-solution: unrecognized solver output: #<eof>
--------------------

non-empty stderr
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/convenience.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/lens.rkt")
lens.rkt: racket test: #<<non-empty stderr
--------------------
symbolic
ERROR
name:       check-pred
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/lens.rkt:19:2

read-solution: unrecognized solver output: #<eof>
--------------------

non-empty stderr
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/serialization.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/basic.rkt")
basic.rkt: racket test: #<<non-empty stderr
--------------------
basic verification: when enable and reset are not set, value doesn't change
ERROR
name:       check-pred
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/basic.rkt:13:2

error writing to stream port
  system error: Broken pipe; errno=32
--------------------
--------------------
basic verification: counter wraparound even when no reset
ERROR

read-solution: unrecognized solver output: #<eof>
--------------------

non-empty stderr
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/constructor.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/lib.rkt")
lib.rkt: racket test: #<<non-empty stderr
--------------------
if
ERROR
name:       check-equal?
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/lib.rkt:15:2

read-solution: unrecognized solver output: #<eof>
--------------------
--------------------
xor
ERROR
name:       check-pred
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/lib.rkt:26:2

read-solution: unrecognized solver output: #<eof>
--------------------

non-empty stderr
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/memoize.rkt")
memoize.rkt: racket test: #<<non-empty stderr
--------------------
multi-port memory (context-sensitive symbolics)
ERROR

read-solution: unrecognized solver output: #<eof>
--------------------

non-empty stderr
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/metadata.rkt")
metadata.rkt: racket test: #<<non-empty stderr
--------------------
using auto-generated methods
ERROR
name:       check-pred
location:
  /home/root/user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/metadata.rkt:14:2

error writing to stream port
  system error: Broken pipe; errno=32
--------------------

non-empty stderr
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/uf.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/counter.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/lockbox.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/multi_port_memory.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/picorv32.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/print-test.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/ram.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/use_persistent_reset.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/zeroinit.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/core.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/debug/expand/lang/reader.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/debug/expand.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/debug/read/lang/reader.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/debug/read.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/generic.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/lang/configure-runtime.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/lang/reader.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/lib.rkt")
raco test: (submod (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/libopt.rkt") test)
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/main.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/memoize.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/meta.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/parameters.rkt")
raco test: (submod (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/reader.rkt") test)
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/verilog.rkt")
raco test: (file "/home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/yosys.rkt")
  12 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/serialization.rkt
  11 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/reader.rkt
   6 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/addressable-struct.rkt
   3 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/substitution.rkt
   3 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/knox/driver/interpreter.rkt
   2 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/convenience.rkt
   2 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/constructor.rkt
   2 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/uf.rkt
   2 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/zeroinit.rkt
   2 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/libopt.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/info.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/circuit/circuit-lang.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/circuit/lang/reader.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/circuit.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/checker.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/correctness-lang.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/correctness.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/hint.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/correctness/lang/reader.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver/driver-lang.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver/interpreter.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver/lang/reader.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver/lib.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/driver.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator/emulator-lang.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator/lang/reader.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator/util.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/result.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/security/checker.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/security/lang/reader.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/security/security-lang.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/environment.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/lifted.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/shared.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/syntax.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/semantics/value.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/spec/lang/reader.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/spec/spec-lang.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/spec.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/addressable-struct.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/concretize.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/convenience.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/dependence.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/lens.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/main.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/overapproximate.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/serialization.rkt9/54 test failures

   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/util.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/info.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/knox/circuit/use_persistent_reset.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/counter.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/lockbox.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/multi_port_memory.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/picorv32.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/print-test.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/ram.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/verilog/use_persistent_reset.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/core.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/debug/expand/lang/reader.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/debug/expand.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/debug/read/lang/reader.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/debug/read.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/generic.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/lang/configure-runtime.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/lang/reader.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/lib.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/main.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/memoize.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/meta.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/parameters.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/verilog.rkt
   0 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/yosys/yosys.rkt
1  1 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/knox/emulator/interpreter.rkt
1  1 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/rosutil/subsumption.rkt
1  1 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/knox/circuit.rkt
1  1 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/concretize.rkt
1  1 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/rosutil/lens.rkt
1  1 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/basic.rkt
1  1 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/lib.rkt
1  1 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/memoize.rkt
1  1 /home/root//user/.local/share/racket/8.17.0.4/pkgs/knox/test/yosys/metadata.rkt
The time is now Sunday, June 15th, 2025 8:29:01pm