Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Panic with "expected Integer intModUnOp" #114

Closed
brianhuffman opened this issue Dec 10, 2020 · 0 comments · Fixed by #115
Closed

Panic with "expected Integer intModUnOp" #114

brianhuffman opened this issue Dec 10, 2020 · 0 comments · Fixed by #115

Comments

@brianhuffman
Copy link
Contributor

The error manifests when you use an SBV proof backend on a term that uses negation on a Z type:

sawscript> prove z3 {{ (2:Z 7) == -5 }}

You have encountered a bug in SawCore's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-core/issues

%< ---------------------------------------------------
  Revision:  ea3a62840f5a250e0a3f64ce20790f3b54206565
  Branch:    text-fieldname (uncommited files present)
  Location:  Verifier.SAW.Simulator.Prims
  Message:   expected Integer intModUnOp
CallStack (from HasCallStack):
  panic, called at src/Verifier/SAW/Utils.hs:37:9 in saw-core-0.1-DyYEChKwXD86nNPWWACPrn:Verifier.SAW.Utils
  panic, called at src/Verifier/SAW/Simulator/Prims.hs:268:13 in saw-core-0.1-DyYEChKwXD86nNPWWACPrn:Verifier.SAW.Simulator.Prims
  panic, called at src/Verifier/SAW/Simulator/Prims.hs:298:15 in saw-core-0.1-DyYEChKwXD86nNPWWACPrn:Verifier.SAW.Simulator.Prims
%< ---------------------------------------------------

Thanks to @msaaltink for reporting this.

brianhuffman pushed a commit that referenced this issue Dec 10, 2020
This was an unintentional omission from PR #93, which correctly
updated `intModUnOp` in the what4 backend, but not in sbv.

Fixes #114.
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant