SBV error: invalid function declaration reference, unknown function -1 AND w4 error: arithmetic underflow

[weaversa]

Here's a simple Cryptol function that causes some issues w/ SAW.

$ cat a.cry
f : [2] -> [10]
f x = take y
  where
    y = x # y

Everything works correctly within Cryptol...

$ cryptol a.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.13.0.99
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Main
Main> f 0b11
0x3ff
Main> f 0b00
0x000
Main> f 0b10
0x2aa
Main> :sat \x -> f x == zero
Satisfiable
(\x -> f x == zero) 0x0 = True
(Total Elapsed Time: 0.046s, using "Z3")

But when we get to saw we get some errors with both the SBV and what4 backends.

SBV:

$ saw
 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 0.9.0.99 (<non-dev-build>)

sawscript> import "a.cry"
sawscript> print {{ f 0b11 }}
[17:04:08.804] 768
sawscript> print {{ f 0b10 }}
[17:04:11.592] 512
sawscript> print {{ f 0b00 }}
[17:04:14.520] 0
sawscript> sat z3 {{ \x -> f x == zero }}


*** Data.SBV: Unexpected non-success response from Z3:
***
***    Sent      : (define-fun s10 () (_ BitVec 1) ((_ extract -1 -1) s0))
***    Expected  : success
***    Received  : (error "line 18 column 44: invalid function declaration reference, unknown function -1")
***
***    Exit code : ExitFailure (-15)
***    Executable: /usr/local/bin/z3
***    Options   : -nw -in -smt2
***
***    Reason    : Check solver response for further information. If your code is correct,
***                please report this as an issue either with SBV or the solver itself!

what4:

sawscript> sat (w4_unint_z3 []) {{ \x -> f x == zero }}

arithmetic underflow

[RyanGlScott]

Good catch! It turns out that saw-core doesn't quite implement the atWithDefault function (i.e., saw-core's equivalent of (@)) correctly for bit sequences when the index exceeds the bit width. (It does implement it correctly for other types of sequences, which is perhaps why we never noticed this before.) I've opened #1773 with a fix.