k: [Bug] test case failure in proof-tests
One test case still fails on my machine (macos11)
Running make -C proof-tests, the following command gets run, producing the diff output below:
/Users/brucecollie/code/k/k-distribution/bin/kprove deposit-spec.k --smt-prelude imap.smt2 --no-exc-wrap -d . | sed 's!'`pwd`'/\(\./\)\{0,2\}!!g' | diff - deposit-spec.k.out
1,17c1
< <T>
< <k>
< tn ( V0 , V1 , up ( V1 , V0 +Int 1 ) ) ~> V2
< </k>
< <zerohashes>
< V3
< </zerohashes>
< <branch>
< V4
< </branch>
< <depositCount>
< V0
< </depositCount>
< <treeHeight>
< V5
< </treeHeight>
< </T>
---
> #Top
About this issue
- Original URL
- State: closed
- Created 3 years ago
- Comments: 15 (15 by maintainers)
Commits related to this issue
- Add explicit to_int cast to ^Int SMT hook This was recommended as a workaround for #2154 and #1957 by the Z3 maintainers (https://github.com/Z3Prover/z3/issues/5243). The original issue arises becau... — committed to runtimeverification/k by Baltoli 3 years ago
- Add explicit to_int cast to ^Int SMT hook This was recommended as a workaround for #2154 and #1957 by the Z3 maintainers (https://github.com/Z3Prover/z3/issues/5243). The original issue arises becau... — committed to runtimeverification/k by Baltoli 3 years ago
@Baltoli can you isolate the Z3 query that is actually causing the problem? You can do
--solver-transcript FILE_NAMEto produce a transcript of the Z3 queries that the Haskell backend is sending, and you can check which one behaves differently on 4.8.7 vs later versions.--solver-transcriptis akore-execoption, so you may need to use--haskell-backend-command ...argument tokproveto make this work (or to set env variableKORE_EXEC_OPTS).Ask on slack for more info. Getting solver transcripts is worth learning how to do.