Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

goal_eval_unint failure with tuple-typed variables #561

Closed
brianhuffman opened this issue Oct 3, 2019 · 1 comment
Closed

goal_eval_unint failure with tuple-typed variables #561

brianhuffman opened this issue Oct 3, 2019 · 1 comment
Assignees
Labels
type: bug Issues reporting bugs or unexpected/unwanted behavior

Comments

@brianhuffman
Copy link
Contributor

The following saw-script:

let {{
  foo : ([8],[64]) -> [16] -> ([8],[64])
  foo x y = x
}};

let tac =
  do {
    goal_eval_unint ["foo"];
    z3;
  };

prove tac {{ \x -> foo x zero == x }};

fails with a panic:

[15:50:14.510] Loading file "/Users/huffman/Documents/saw/goal_eval.saw"
[15:50:14.545] You have encountered a bug in Crucible's implementation.
*** Please create an issue at https://github.com/GaloisInc/crucible/issues

%< ---------------------------------------------------
  Revision:  a4c77ca2932b012e130378c1f0f72be0af0bb888
  Branch:    HEAD (uncommited files present)
  Location:  SAWCore.applyExprSymFn
  Message:   Unknown symbolic function.
             *** Name: x_L
CallStack (from HasCallStack):
  panic, called at src/Lang/Crucible/Panic.hs:11:9 in crucible-0.5-7B7TzoUKryl3ikgTNQA4f2:Lang.Crucible.Panic
  panic, called at src/Lang/Crucible/Backend/SAWCore.hs:712:21 in crucible-saw-0.1-5HtkMLBRiPeHJyebZADtzS:Lang.Crucible.Backend.SAWCore
%< ---------------------------------------------------
@brianhuffman brianhuffman added the type: bug Issues reporting bugs or unexpected/unwanted behavior label Oct 18, 2019
@brianhuffman brianhuffman self-assigned this Dec 9, 2020
@brianhuffman
Copy link
Contributor Author

Fixed in #601, which includes GaloisInc/saw-core-what4@fd1f993 and GaloisInc/saw-core-sbv@414d7b3.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

No branches or pull requests

1 participant