Search results

The syntax of sawscript import does not match the documentation.

documentationIssues involving documentationIssues involving documentation

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

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: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

Status: Open.

#3310 In GaloisInc/saw-script;

· mtullsen opened on Jun 18, 2026

crux-mir-comp running with --branch-coverage flag significantly slower

Status: Open.

#3309 In GaloisInc/saw-script;

· podhrmic opened on Jun 18, 2026

crux-mir-comp regression: using overrides tanks performance

performanceIssues that involve or include performance problemsIssues that involve or include performance problems

regressionSomething that used to work, but now doesn'tSomething that used to work, but now doesn't

subsystem: crucible-mir-compIssues related to compositional Rust verification with crucible-mir-comp or crux-mir-compIssues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp

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

Status: Open.

#3308 In GaloisInc/saw-script;

· RyanGlScott opened on Jun 16, 2026

·  

current: advanced

offline_w4_unint_yices always fails

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

Status: Open.

#3304 In GaloisInc/saw-script;

· RyanGlScott opened on Jun 12, 2026

Proof tactic combinators

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: proofsIssues about the proof system or proof sequentsIssues about the proof system or proof sequents

topics: error-handlingIssues involving the way SAW responds to an error conditionIssues involving the way SAW responds to an error condition

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.

#3300 In GaloisInc/saw-script;

· brianhuffman opened on Jun 8, 2026

·  

current: advanced

Support calls using/omitting nest parameter attributes

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

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

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

Status: Open.

#3299 In GaloisInc/saw-script;

· kquick opened on Jun 8, 2026

x86 verification is missing detectVacuity support

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: x86Issues related to verifying x86 binaries via MacawIssues related to verifying x86 binaries via Macaw

topics: error-handlingIssues involving the way SAW responds to an error conditionIssues involving the way SAW responds to an error condition

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.

#3289 In GaloisInc/saw-script;

· sauclovian-g opened on May 29, 2026

·  

current: normal

ProofScript sequents require a large complex API

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

subsystem: proofsIssues about the proof system or proof sequentsIssues about the proof system or proof sequents

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: 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.

#3281 In GaloisInc/saw-script;

· brianhuffman opened on May 26, 2026

·  

current: advanced

specialize_theorem should have pure function type

Status: Open.

#3278 In GaloisInc/saw-script;

· brianhuffman opened on May 22, 2026

The run builtin is unsound if used in the ProofScript context

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

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: bugIssues reporting bugs or unexpected/unwanted behaviorIssues reporting bugs or unexpected/unwanted behavior

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

Status: Open.

#3271 In GaloisInc/saw-script;

· sauclovian-g opened on May 21, 2026

·  

current: advanced

SAW proof tactics used to let you prove False

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

subsystem: proofsIssues about the proof system or proof sequentsIssues about the proof system or proof sequents

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

Status: Open.

#3270 In GaloisInc/saw-script;

· brianhuffman opened on May 21, 2026

·  

current: severe

SAW fails to prove lemmas about modular exponentiation that Cryptol handles easily

missing cryptol featuresIssues about features in Cryptol that don't work in SAWIssues about features in Cryptol that don't work in SAW

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

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

Status: Open.

#3263 In GaloisInc/saw-script;

· brianhuffman opened on May 19, 2026

·  

current: advanced