Search results

Deprecate assume_unsat

subsystem: saw-scriptIssues related to the SAWScript language and/or its interpretation and executionIssues related to the SAWScript language and/or its interpretation and execution

tech debtIssues that document or involve technical debtIssues that document or involve technical debt

type: enhancementIssues describing an improvement to an existing feature or capabilityIssues describing an improvement to an existing feature or capability

Status: Open.

#3223 In GaloisInc/saw-script;

· brianhuffman opened on May 5, 2026

·  

current: normal

Move some theorems and axioms about bvAdd into the SAWCore prelude

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: enhancementIssues describing an improvement to an existing feature or capabilityIssues describing an improvement to an existing feature or capability

Status: Open.

#3222 In GaloisInc/saw-script;

· brianhuffman opened on May 5, 2026

·  

current: advanced

unfolding_fix_once is unable to prove a simple theorem about a recursive function

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

Status: Open.

#3218 In GaloisInc/saw-script;

· brianhuffman opened on May 4, 2026

·  

current: advanced

REPL :search should be able to include name patterns

needs designTechnical design work is needed for issue to progressTechnical design work is needed for issue to progress

subsystem: saw-scriptIssues related to the SAWScript language and/or its interpretation and executionIssues related to the SAWScript language and/or its interpretation and execution

type: enhancementIssues describing an improvement to an existing feature or capabilityIssues describing an improvement to an existing feature or capability

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3217 In GaloisInc/saw-script;

· sauclovian-g opened on May 4, 2026

·  

current: normal

Unify and generalize functions add_prelude_eqs/add_cryptol_eqs and add_prelude_defs/add_cryptol_defs

needs designTechnical design work is needed for issue to progressTechnical design work is needed for issue to progress

needs testIssues for which we should add a regression testIssues for which we should add a regression test

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

topics: saw-core namesIssues related to URI-based saw-core namesIssues related to URI-based saw-core names

type: enhancementIssues describing an improvement to an existing feature or capabilityIssues describing an improvement to an existing feature or capability

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3213 In GaloisInc/saw-script;

· brianhuffman opened on May 1, 2026

·  

current: normal

Implement means to browse/query/search the set of defined SAWCore names

subsystem: cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-core

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: feature requestIssues requesting a new feature or capabilityIssues requesting a new feature or capability

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3212 In GaloisInc/saw-script;

· brianhuffman opened on May 1, 2026

·  

current: normal

prove and prove_print should work with SAWCore terms of type Prop

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3211 In GaloisInc/saw-script;

· brianhuffman opened on May 1, 2026

·  

current: normal

parseUninterpretedSAW seems to be wrong for rationals.

needs testIssues for which we should add a regression testIssues for which we should add a regression test

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

Status: Open.

#3206 In GaloisInc/saw-script;

· yav opened on Apr 28, 2026

·  

current: normal

Feature request: Report on all uses of unsafeAssert in imported Cryptol terms

subsystem: cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-core

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

type: enhancementIssues describing an improvement to an existing feature or capabilityIssues describing an improvement to an existing feature or capability

unsoundnessIssues that can lead to unsoundness or false verificationIssues that can lead to unsoundness or false verification

Status: Open.

#3205 In GaloisInc/saw-script;

· brianhuffman opened on Apr 28, 2026

·  

current: advanced

Malformed term in test_cryptol_module_sha512

subsystem: cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-coreIssues related to Cryptol -> saw-core translation with cryptol-saw-core

subsystem: saw-coreIssues related to the saw-core representation or the saw-core subsystemIssues related to the saw-core representation or the saw-core subsystem

subsystem: saw-core-rocqIssues related to converting saw-core to Gallina for use with the Rocq theorem proverIssues related to converting saw-core to Gallina for use with the Rocq theorem prover

tech debtIssues that document or involve technical debtIssues that document or involve technical debt

type: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

Status: Open.

#3198 In GaloisInc/saw-script;

· sauclovian-g opened on Apr 25, 2026

·  

current: normal

There should be functions for extracting the LLVM/JVM/MIR types of LLVm/JVM/MIR values

needs testIssues for which we should add a regression testIssues for which we should add a regression test

subsystem: crucible-jvmIssues related to Java verification with crucible-jvmIssues related to Java verification with crucible-jvm

subsystem: crucible-llvmIssues related to LLVM bitcode verification with crucible-llvmIssues related to LLVM bitcode verification with crucible-llvm

subsystem: crucible-mirIssues related to Rust verification with crucible-mir and/or mir-jsonIssues related to Rust verification with crucible-mir and/or mir-json

subsystem: saw-scriptIssues related to the SAWScript language and/or its interpretation and executionIssues related to the SAWScript language and/or its interpretation and execution

type: feature requestIssues requesting a new feature or capabilityIssues requesting a new feature or capability

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3194 In GaloisInc/saw-script;

· sauclovian-g opened on Apr 24, 2026

·  

Someday

There is no jvm_fresh_cryptol_var

easyIssues that are expected to be easy to resolve and might therefore be good for new contributorsIssues that are expected to be easy to resolve and might therefore be good for new contributors

needs testIssues for which we should add a regression testIssues for which we should add a regression test

subsystem: crucible-jvmIssues related to Java verification with crucible-jvmIssues related to Java verification with crucible-jvm

tech debtIssues that document or involve technical debtIssues that document or involve technical debt

type: enhancementIssues describing an improvement to an existing feature or capabilityIssues describing an improvement to an existing feature or capability

usabilityAn issue that impedes efficient understanding and useAn issue that impedes efficient understanding and use

Status: Open.

#3192 In GaloisInc/saw-script;

· sauclovian-g opened on Apr 24, 2026

·  

Someday