Skip to content

Trailing parenthesis in sexpression comment #102

Closed
#103
Closed
Trailing parenthesis in sexpression comment#102
#103

Description

@philzook58
philzook58
opened on Jul 23, 2026

The closing parenthesis that closes (trace at the very end of this example is inside the comment (assert (not v379)) ; 0:0 - 0:0).

$ nix develop path:. --command isla-footprint \
  -A isla-snapshots/rv32d.ir \
  -C riscv32.toml \
  -i 6304b500 \
  -x -e little -s --executable \
  -T 1 --timeout 20 \
  -R PC=0x00001000 \
  -R nextPC=0x00001004
No primop parse_hex_bits (Name { id: 2604 })
No primop emulator_write_tag (Name { id: 2906 })
No primop emulator_read_tag (Name { id: 2905 })
No primop sys_enable_experimental_extensions (Name { id: 2831 })
No primop sys_enable_experimental_extensions (Name { id: 2831 })
No primop valid_reservation (Name { id: 4247 })
(trace
  (assume-reg |__monomorphize_reads| nil false)
  (assume-reg |__monomorphize_writes| nil false)
  (assume-reg |misa| nil (_ struct (|bits| #x00000000)))
  (assume-reg |mstatus| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mseccfg| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |menvcfg| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |senvcfg| nil (_ struct (|bits| #x00000000)))
  (assume-reg |mcountinhibit| nil (_ struct (|bits| #x00000000)))
  (assume-reg |mvendorid| nil #x00000000)
  (assume-reg |mimpid| nil #x00000000)
  (assume-reg |marchid| nil #x00000000)
  (assume-reg |mhartid| nil #x00000000)
  (assume-reg |mconfigptr| nil #x00000000)
  (assume-reg |mstateen0| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mstateen1| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mstateen2| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mstateen3| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |hstateen0| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |hstateen1| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |hstateen2| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |hstateen3| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |sstateen0| nil (_ struct (|bits| #x00000000)))
  (assume-reg |sstateen1| nil (_ struct (|bits| #x00000000)))
  (assume-reg |sstateen2| nil (_ struct (|bits| #x00000000)))
  (assume-reg |sstateen3| nil (_ struct (|bits| #x00000000)))
  (assume-reg |mcyclecfg| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |minstretcfg| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |sig_meip| nil #b0)
  (assume-reg |sig_seip| nil #b0)
  (assume-reg |pc_reset_address| nil #x00000000)
  (assume-reg |htif_tohost_base| nil (|None| (_ unit)))
  (assume-reg |mtimecmp| nil #x0000000000000000)
  (assume-reg |stimecmp| nil #x0000000000000000)
  (assume-reg |htif_tohost| nil #x0000000000000000)
  (assume-reg |htif_done| nil false)
  (assume-reg |htif_exit_code| nil #x0000000000000000)
  (assume-reg |htif_cmd_write| nil #b0)
  (assume-reg |htif_payload_writes| nil #x0)
  (assume-reg |pma_regions| nil (_ list (_ struct (|base| #x0000000080000000) (|attributes| (_ struct (|read_idempotent| true) (|atomic_support| |AMOCASQ|) (|coherent| true) (|cacheable| true) (|readable| true) (|reservability| |RsrvEventual|) (|mem_type| |MainMemory|) (|misaligned_exceptions| (_ struct (|load_store| (|None| (_ unit))) (|amo| |AccessFault|) (|vector| (|None| (_ unit))))) (|supports_cbo_zero| true) (|supports_pte_read| true) (|writable| true) (|write_idempotent| true) (|supports_pte_write| true) (|executable| true))) (|include_in_device_tree| true) (|size| #x0000000080000000)) (_ struct (|size| #x0000000010000000) (|attributes| (_ struct (|supports_pte_write| false) (|executable| false) (|cacheable| false) (|writable| true) (|atomic_support| |AMONone|) (|misaligned_exceptions| (_ struct (|load_store| (|None| (_ unit))) (|vector| (|None| (_ unit))) (|amo| |AccessFault|))) (|read_idempotent| false) (|mem_type| |IOMemory|) (|readable| true) (|reservability| |RsrvNone|) (|supports_pte_read| false) (|write_idempotent| false) (|supports_cbo_zero| false) (|coherent| true))) (|base| #x0000000002000000) (|include_in_device_tree| false)) (_ struct (|include_in_device_tree| false) (|attributes| (_ struct (|cacheable| true) (|coherent| false) (|mem_type| |IOMemory|) (|atomic_support| |AMONone|) (|read_idempotent| true) (|reservability| |RsrvNone|) (|writable| false) (|write_idempotent| true) (|executable| false) (|misaligned_exceptions| (_ struct (|load_store| (|None| (_ unit))) (|vector| (|None| (_ unit))) (|amo| |AccessFault|))) (|supports_cbo_zero| false) (|supports_pte_read| false) (|readable| true) (|supports_pte_write| false))) (|base| #x0000000000001000) (|size| #x0000000000001000))))
  (assume-reg |tlb| nil (_ vec (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit))))
  (assume-reg |satp| nil #x00000000)
  (assume-reg |ssp| nil #x00000000)
  (assume-reg |hart_state| nil (|HART_ACTIVE| (_ unit)))
  (define-enum |MemoryRegionType| 2 (|MainMemory| |IOMemory|)) ; 0:0 - 0:0
  (define-enum |AtomicSupport| 7 (|AMONone| |AMOSwap| |AMOLogical| |AMOArithmetic| |AMOCASW| |AMOCASD| |AMOCASQ|)) ; 0:0 - 0:0
  (define-enum |Reservability| 3 (|RsrvNone| |RsrvNonEventual| |RsrvEventual|)) ; 0:0 - 0:0
  (define-enum |vector_support| 5 (|Disabled| |Integer| |Float_single| |Float_double| |Full|)) ; 0:0 - 0:0
  (define-enum |extension| 120 (|Ext_M| |Ext_A| |Ext_F| |Ext_D| |Ext_B| |Ext_V| |Ext_S| |Ext_U| |Ext_H| |Ext_Zibi| |Ext_Zic64b| |Ext_Zicbom| |Ext_Zicbop| |Ext_Zicboz| |Ext_Zicfilp| |Ext_Zicfiss| |Ext_Zicntr| |Ext_Zicond| |Ext_Zicsr| |Ext_Zifencei| |Ext_Zihintntl| |Ext_Zihintpause| |Ext_Zihpm| |Ext_Zimop| |Ext_Zmmul| |Ext_Zaamo| |Ext_Zabha| |Ext_Zacas| |Ext_Zalrsc| |Ext_Zawrs| |Ext_Za64rs| |Ext_Za128rs| |Ext_Zfa| |Ext_Zfbfmin| |Ext_Zfh| |Ext_Zfhmin| |Ext_Zfinx| |Ext_Zdinx| |Ext_Zca| |Ext_Zcb| |Ext_Zcd| |Ext_Zcf| |Ext_Zcmop| |Ext_C| |Ext_Zba| |Ext_Zbb| |Ext_Zbc| |Ext_Zbkb| |Ext_Zbkc| |Ext_Zbkx| |Ext_Zbs| |Ext_Ziccamoa| |Ext_Ziccamoc| |Ext_Ziccif| |Ext_Zicclsm| |Ext_Ziccrse| |Ext_Zknd| |Ext_Zkne| |Ext_Zknh| |Ext_Zkr| |Ext_Zksed| |Ext_Zksh| |Ext_Zkt| |Ext_Zhinx| |Ext_Zhinxmin| |Ext_Zvl32b| |Ext_Zvl64b| |Ext_Zvl128b| |Ext_Zvl256b| |Ext_Zvl512b| |Ext_Zvl1024b| |Ext_Zve32f| |Ext_Zve32x| |Ext_Zve64d| |Ext_Zve64f| |Ext_Zve64x| |Ext_Zvabd| |Ext_Zvfbfmin| |Ext_Zvfbfwma| |Ext_Zvfh| |Ext_Zvfhmin| |Ext_Zvbb| |Ext_Zvbc| |Ext_Zvkb| |Ext_Zvkg| |Ext_Zvkned| |Ext_Zvknha| |Ext_Zvknhb| |Ext_Zvksed| |Ext_Zvksh| |Ext_Zvkt| |Ext_Zvkn| |Ext_Zvknc| |Ext_Zvkng| |Ext_Zvks| |Ext_Zvksc| |Ext_Zvksg| |Ext_Ssccptr| |Ext_Sscofpmf| |Ext_Sscounterenw| |Ext_Ssstateen| |Ext_Sstc| |Ext_Sstvala| |Ext_Sstvecd| |Ext_Ssu64xl| |Ext_Svbare| |Ext_Sv32| |Ext_Sv39| |Ext_Sv48| |Ext_Sv57| |Ext_Svade| |Ext_Svadu| |Ext_Svinval| |Ext_Svnapot| |Ext_Svpbmt| |Ext_Svrsw60t59b| |Ext_Svvptc| |Ext_Smcntrpmf| |Ext_Smstateen| |Ext_Ssqosid|)) ; 0:0 - 0:0
  (define-enum |misaligned_exception| 2 (|AccessFault| |AlignmentException|)) ; 0:0 - 0:0
  (define-enum |Privilege| 5 (|User| |VirtualUser| |Supervisor| |VirtualSupervisor| |Machine|)) ; 0:0 - 0:0
  (define-enum |PmpAddrMatchType| 4 (|OFF| |TOR| |NA4| |NAPOT|)) ; 0:0 - 0:0
  (define-enum |landing_pad_expectation| 2 (|NO_LP_EXPECTED| |LP_EXPECTED|)) ; 0:0 - 0:0
  (assume-reg |PC| nil #x00001000)
  (assume-reg |nextPC| nil #x00001004)
  (cycle)
  (read-reg |cur_privilege| nil |Machine|)
  (read-reg |mseccfg| nil (_ struct (|bits| #x0000000000000000)))
  (define-enum |bop| 6 (|BEQ| |BNE| |BLT| |BGE| |BLTU| |BGEU|)) ; 0:0 - 0:0
  (declare-const v377 (_ BitVec 32)) ; core/regs.sail 164:12 - 164:15
  (read-reg |x10| nil v377)
  (declare-const v378 (_ BitVec 32)) ; core/regs.sail 165:12 - 165:15
  (read-reg |x11| nil v378)
  (define-const v379 (= v377 v378)) ; extensions/I/base_insts.sail 118:12 - 118:28
  (branch 0 "extensions/I/base_insts.sail 125:2 - 127:21")
  (assert v379) ; 0:0 - 0:0
  (read-reg |PC| nil #x00001000)
  (branch-address #x00001008)
  (write-reg |nextPC| nil #x00001008))
(trace
  (assume-reg |__monomorphize_reads| nil false)
  (assume-reg |__monomorphize_writes| nil false)
  (assume-reg |misa| nil (_ struct (|bits| #x00000000)))
  (assume-reg |mstatus| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mseccfg| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |menvcfg| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |senvcfg| nil (_ struct (|bits| #x00000000)))
  (assume-reg |mcountinhibit| nil (_ struct (|bits| #x00000000)))
  (assume-reg |mvendorid| nil #x00000000)
  (assume-reg |mimpid| nil #x00000000)
  (assume-reg |marchid| nil #x00000000)
  (assume-reg |mhartid| nil #x00000000)
  (assume-reg |mconfigptr| nil #x00000000)
  (assume-reg |mstateen0| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mstateen1| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mstateen2| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |mstateen3| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |hstateen0| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |hstateen1| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |hstateen2| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |hstateen3| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |sstateen0| nil (_ struct (|bits| #x00000000)))
  (assume-reg |sstateen1| nil (_ struct (|bits| #x00000000)))
  (assume-reg |sstateen2| nil (_ struct (|bits| #x00000000)))
  (assume-reg |sstateen3| nil (_ struct (|bits| #x00000000)))
  (assume-reg |mcyclecfg| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |minstretcfg| nil (_ struct (|bits| #x0000000000000000)))
  (assume-reg |sig_meip| nil #b0)
  (assume-reg |sig_seip| nil #b0)
  (assume-reg |pc_reset_address| nil #x00000000)
  (assume-reg |htif_tohost_base| nil (|None| (_ unit)))
  (assume-reg |mtimecmp| nil #x0000000000000000)
  (assume-reg |stimecmp| nil #x0000000000000000)
  (assume-reg |htif_tohost| nil #x0000000000000000)
  (assume-reg |htif_done| nil false)
  (assume-reg |htif_exit_code| nil #x0000000000000000)
  (assume-reg |htif_cmd_write| nil #b0)
  (assume-reg |htif_payload_writes| nil #x0)
  (assume-reg |pma_regions| nil (_ list (_ struct (|base| #x0000000080000000) (|attributes| (_ struct (|read_idempotent| true) (|atomic_support| |AMOCASQ|) (|coherent| true) (|cacheable| true) (|readable| true) (|reservability| |RsrvEventual|) (|mem_type| |MainMemory|) (|misaligned_exceptions| (_ struct (|load_store| (|None| (_ unit))) (|amo| |AccessFault|) (|vector| (|None| (_ unit))))) (|supports_cbo_zero| true) (|supports_pte_read| true) (|writable| true) (|write_idempotent| true) (|supports_pte_write| true) (|executable| true))) (|include_in_device_tree| true) (|size| #x0000000080000000)) (_ struct (|size| #x0000000010000000) (|attributes| (_ struct (|supports_pte_write| false) (|executable| false) (|cacheable| false) (|writable| true) (|atomic_support| |AMONone|) (|misaligned_exceptions| (_ struct (|load_store| (|None| (_ unit))) (|vector| (|None| (_ unit))) (|amo| |AccessFault|))) (|read_idempotent| false) (|mem_type| |IOMemory|) (|readable| true) (|reservability| |RsrvNone|) (|supports_pte_read| false) (|write_idempotent| false) (|supports_cbo_zero| false) (|coherent| true))) (|base| #x0000000002000000) (|include_in_device_tree| false)) (_ struct (|include_in_device_tree| false) (|attributes| (_ struct (|cacheable| true) (|coherent| false) (|mem_type| |IOMemory|) (|atomic_support| |AMONone|) (|read_idempotent| true) (|reservability| |RsrvNone|) (|writable| false) (|write_idempotent| true) (|executable| false) (|misaligned_exceptions| (_ struct (|load_store| (|None| (_ unit))) (|vector| (|None| (_ unit))) (|amo| |AccessFault|))) (|supports_cbo_zero| false) (|supports_pte_read| false) (|readable| true) (|supports_pte_write| false))) (|base| #x0000000000001000) (|size| #x0000000000001000))))
  (assume-reg |tlb| nil (_ vec (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit)) (|None| (_ unit))))
  (assume-reg |satp| nil #x00000000)
  (assume-reg |ssp| nil #x00000000)
  (assume-reg |hart_state| nil (|HART_ACTIVE| (_ unit)))
  (define-enum |MemoryRegionType| 2 (|MainMemory| |IOMemory|)) ; 0:0 - 0:0
  (define-enum |AtomicSupport| 7 (|AMONone| |AMOSwap| |AMOLogical| |AMOArithmetic| |AMOCASW| |AMOCASD| |AMOCASQ|)) ; 0:0 - 0:0
  (define-enum |Reservability| 3 (|RsrvNone| |RsrvNonEventual| |RsrvEventual|)) ; 0:0 - 0:0
  (define-enum |vector_support| 5 (|Disabled| |Integer| |Float_single| |Float_double| |Full|)) ; 0:0 - 0:0
  (define-enum |extension| 120 (|Ext_M| |Ext_A| |Ext_F| |Ext_D| |Ext_B| |Ext_V| |Ext_S| |Ext_U| |Ext_H| |Ext_Zibi| |Ext_Zic64b| |Ext_Zicbom| |Ext_Zicbop| |Ext_Zicboz| |Ext_Zicfilp| |Ext_Zicfiss| |Ext_Zicntr| |Ext_Zicond| |Ext_Zicsr| |Ext_Zifencei| |Ext_Zihintntl| |Ext_Zihintpause| |Ext_Zihpm| |Ext_Zimop| |Ext_Zmmul| |Ext_Zaamo| |Ext_Zabha| |Ext_Zacas| |Ext_Zalrsc| |Ext_Zawrs| |Ext_Za64rs| |Ext_Za128rs| |Ext_Zfa| |Ext_Zfbfmin| |Ext_Zfh| |Ext_Zfhmin| |Ext_Zfinx| |Ext_Zdinx| |Ext_Zca| |Ext_Zcb| |Ext_Zcd| |Ext_Zcf| |Ext_Zcmop| |Ext_C| |Ext_Zba| |Ext_Zbb| |Ext_Zbc| |Ext_Zbkb| |Ext_Zbkc| |Ext_Zbkx| |Ext_Zbs| |Ext_Ziccamoa| |Ext_Ziccamoc| |Ext_Ziccif| |Ext_Zicclsm| |Ext_Ziccrse| |Ext_Zknd| |Ext_Zkne| |Ext_Zknh| |Ext_Zkr| |Ext_Zksed| |Ext_Zksh| |Ext_Zkt| |Ext_Zhinx| |Ext_Zhinxmin| |Ext_Zvl32b| |Ext_Zvl64b| |Ext_Zvl128b| |Ext_Zvl256b| |Ext_Zvl512b| |Ext_Zvl1024b| |Ext_Zve32f| |Ext_Zve32x| |Ext_Zve64d| |Ext_Zve64f| |Ext_Zve64x| |Ext_Zvabd| |Ext_Zvfbfmin| |Ext_Zvfbfwma| |Ext_Zvfh| |Ext_Zvfhmin| |Ext_Zvbb| |Ext_Zvbc| |Ext_Zvkb| |Ext_Zvkg| |Ext_Zvkned| |Ext_Zvknha| |Ext_Zvknhb| |Ext_Zvksed| |Ext_Zvksh| |Ext_Zvkt| |Ext_Zvkn| |Ext_Zvknc| |Ext_Zvkng| |Ext_Zvks| |Ext_Zvksc| |Ext_Zvksg| |Ext_Ssccptr| |Ext_Sscofpmf| |Ext_Sscounterenw| |Ext_Ssstateen| |Ext_Sstc| |Ext_Sstvala| |Ext_Sstvecd| |Ext_Ssu64xl| |Ext_Svbare| |Ext_Sv32| |Ext_Sv39| |Ext_Sv48| |Ext_Sv57| |Ext_Svade| |Ext_Svadu| |Ext_Svinval| |Ext_Svnapot| |Ext_Svpbmt| |Ext_Svrsw60t59b| |Ext_Svvptc| |Ext_Smcntrpmf| |Ext_Smstateen| |Ext_Ssqosid|)) ; 0:0 - 0:0
  (define-enum |misaligned_exception| 2 (|AccessFault| |AlignmentException|)) ; 0:0 - 0:0
  (define-enum |Privilege| 5 (|User| |VirtualUser| |Supervisor| |VirtualSupervisor| |Machine|)) ; 0:0 - 0:0
  (define-enum |PmpAddrMatchType| 4 (|OFF| |TOR| |NA4| |NAPOT|)) ; 0:0 - 0:0
  (define-enum |landing_pad_expectation| 2 (|NO_LP_EXPECTED| |LP_EXPECTED|)) ; 0:0 - 0:0
  (assume-reg |PC| nil #x00001000)
  (assume-reg |nextPC| nil #x00001004)
  (cycle)
  (read-reg |cur_privilege| nil |Machine|)
  (read-reg |mseccfg| nil (_ struct (|bits| #x0000000000000000)))
  (define-enum |bop| 6 (|BEQ| |BNE| |BLT| |BGE| |BLTU| |BGEU|)) ; 0:0 - 0:0
  (declare-const v377 (_ BitVec 32)) ; core/regs.sail 164:12 - 164:15
  (read-reg |x10| nil v377)
  (declare-const v378 (_ BitVec 32)) ; core/regs.sail 165:12 - 165:15
  (read-reg |x11| nil v378)
  (define-const v379 (= v377 v378)) ; extensions/I/base_insts.sail 118:12 - 118:28
  (branch 0 "extensions/I/base_insts.sail 125:2 - 127:21")
  (assert (not v379)) ; 0:0 - 0:0)

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions