The what4-serialize repository provides a package for serializing what4 terms to an s-expression format (and later de-serializing them). It is very closely tied to the internal representation of what4, and needs to be updated whenever the internals of what4 change.

https://github.com/GaloisInc/what4-serialize

The fp.min and fp.max operations of the SMTLib2 theory of IEEE 754 arithmetic are underspecified WTR to the result when passed in two zeros (of potentially differing signs). The actual IEEE spec itself is underspecified as to which signedness of zero will be returned (CF http://smtlib.cs.uiowa.edu/papers/BTRW14.pdf)

This is, as far as I know, the only place where some "core" operations of the theory are not fully specified (most of the transcendental functions, however, are underspecified WRT the amount of precision they are required to produce).

This is an extremely annoying corner case, but I think we need to deal with it somehow, as solvers actually produce observably different behaviors, as do actual implementations. This could, in principle, yield a soundness issue.

Moreover, Z3 actively punts on this issue by considering, e.g., fp.min (-zero, +zero) to be a value form and will return syntax for this when asked to evaluate values in a model. Our value parsing code can't properly handle these non-standard syntactic forms.

Due to API limitations asConcrete may not work as expected on all arrays. It should handle the case of a constant array correctly but non-constant arrays may not be handled properly. A key part of the issue is that the IsExpr class doesn't provide a way to get at the updates or values that differ from the default value in arrays.

We have the ability to recover literal values from SymExprs for with asNat, asUnsignedBV, asSignedBV, asConstantPred, etc. Is the same thing possible for floats? Could we extract the values of iFloatLit back out? This is a complex question due in part to our various possible interpretations for floating point values (uninterpreted, real, IEEE-754).

Some applications of this would be to pretty-printing and to constant folding.

what4 (bc44c3d) does not declare the sort for a struct used in a forallPred which causes an unknown sort error. Here is a minimal test case:

testForallStruct :: TestTree
testForallStruct = testCase "forall struct" $ withOnlineZ3 $ \sym s -> do
  let repr = viewSome (Some . BaseStructRepr) (Ctx.fromList [Some BaseBoolRepr])
  viewSome (\repr -> do
      var <- freshBoundVar sym (safeSymbol "v") repr
      p0 <- forallPred sym var (truePred sym)
      res <- checkSatisfiable s "test" p0
      isSat res  @? "sat"
    ) repr

Results in:

    Exception: Solver reported an error:
      line 8 column 40: unknown sort 'Struct1'
    in response to command:
      (define-fun x!1 () Bool (forall ((x!0 (Struct1 Bool))) true))

My z3 version (on OS X):

$ z3 --version
Z3 version 4.8.4 - 64 bit

As I work on adding what4 as a new proof backend for Cryptol, one feature I notice that SBV supports that What4 currently does not is computing multiple satisfying assignments for a query.

Given the What4 programming model, it's not immediately clear what's the best way to provide this functionality.

Commit 558d47d changed the traversal operation on expressions so that it descends into the body of defined functions when they appear at call sites. This change was probably a mistake, as it implicitly incorporates the definition of the function directly into the term in which the call site appears. For example, boundVars now returns variables from the definitions of functions, which is quite surprising.

Should this case be realMul?

Similar to #19, What4 currently does not have support for dispatching queries to multiple solvers simultaneously.

Currently we have have realRound, realFloor, and realCeil.

We should also add realTrunc (round toward zero), and realRoundEvent (round to nearest even)

This is a tracking ticket to collect together all the administrivia tasks preceding the 1.0 package release.

Tasks:

• Write a reasonable README
• Start a CHANGELOG
• Check on the status of Hackage documentation, fix any glaring errors/omissions
• Double check .cabal package bounds and update metadata
• Tutorial ?
• Document required/recommended solver versions
• Update copyright notices, license metadata and module headers

The stringIndexOf and stringSubstring functions are not completely faithful to the SMTLib description of their behaviors for out-of-range inputs. We should ensure that we properly follow the exact semantics described here https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

In particular, stringIndexOf should return -1 even for negative and out-of-bounds inputs, and stringSubstring returns the "longest substring no longer than n" when "i+n" is longer than the input string, and returns the empty string if n is negative or i out of range.

PR #89 added a new testing paradigm to the What4 test suite. It generates syntactic templates and uses solvers as a computational oracle to test concrete evaluation of floating-point expressions.

We should extend this idea to other theories, and find some principled way to have these tests run as periodic CI jobs. They are probably too expensive to run on every commit/PR, especially if we extend the test to templates of depth more than 1.

The code for parsing solver results in the What4.Protocol.SMTLib2 module uses fail to indicate parse failures. We should use a more structured error handling mechanism here.

When generating Verilog from What4, the order of inputs in the generated Verilog file is determined by which inputs are discovered first during traversal of the term. This doesn't affect satisfiability, but it does affect the mapping of counter-example or model values back to logical variables.

This affects the SAW w4_abc_verilog command, as can be demonstrated here:

sawscript> sat w4_abc_verilog {{ \(x:[8]) -> \(y:[8]) -> x == 5 /\ y == 2}}
[19:39:41.827] Sat: [x = 5, y = 2]
sawscript> sat w4_abc_verilog {{ \(x:[8]) -> \(y:[8]) -> y == 5 /\ x == 2}}
[19:39:44.436] Sat: [x = 5, y = 2]
sawscript> sat w4_abc_verilog {{ \(x:[8]) -> \(y:[32]) -> y == 0x81050fff /\ x == 2}}
[19:39:51.359] Sat: [x = 255, y = 42009871]
sawscript>

The IORefs that back the What4.Config and What.Expr.Builder modules are significant sources of potential race conditions for multithreaded use, as I discovered when setting up support for portfolio solving. It became necessary to ensure that all the relevant configuration options were set up before forking off threads to supervise the various solvers.

We should audit these datastructures with an eye to multithreading. Many can probably be replaced with MVars instead. For some, we can just ensure we use atomicModifyIORef, etc.

I started a refactoring to implement more realistic symbolic string support in what4, which can be found on the rwd/strings branch.

As I was doing this refactoring, I (re)discovered that string handling is stupid and complicated. The available SMT theories for strings treat strings as a sequence of bytes (as does raw C), but Java wants strings to be sequences of 16-byte unicode codepoints (with some custom encoding for longer codepoints, IIRC), and Haskell's Text datatype assumes UTF-8 encoding, etc.

Doing this correctly will require a lot of care sigh. We'll probably need to implement a family of string representations to actually get the semantics right and it's going to be kind of a mess.

As discussed in GaloisInc/crucible@ed2ffdf and the comments in GaloisInc/crucible#430, there's currently no special handling for passing very large shift amounts to the bvAshr, bvLshr, and bvShl operations. If extremely large shift amounts are passed (e.g. > 0x1000.0000) then this can result in excessive memory consumption or even allocation failures attempting to store these very large Integer values. Actual results for shifting more than the base BV size will generally be 0 anyhow (or possibly -1 for bvAshr).

For any shifts larger than word-width, the semantics should just be to return the 0 value. The rotate operations already to range-reduction via computing remainders, so that's why they don't cause problems.

Attempting to run cabal build all on master will yield the following build errors on what4-abc:

[1 of 1] Compiling What4.Solver.ABC ( src/What4/Solver/ABC.hs, /home/rscott/Documents/Hacking/Haskell/what4-2/dist-newstyle/build/x86_64-linux/ghc-8.10.4/what4-abc-0.1/build/What4/Solver/ABC.o, /home/rscott/Documents/Hacking/Haskell/what4-2/dist-newstyle/build/x86_64-linux/ghc-8.10.4/what4-abc-0.1/build/What4/Solver/ABC.dyn_o )

src/What4/Solver/ABC.hs:747:7: error:
    Not in scope: ‘satQuerySolverName’
    Perhaps you want to add ‘satQuerySolverName’ to the import list
    in the import of ‘What4.Interface’
    (src/What4/Solver/ABC.hs:(81,1)-(82,95)).
    |
747 |     { satQuerySolverName = "ABC"
    |       ^^^^^^^^^^^^^^^^^^

src/What4/Solver/ABC.hs:748:7: error:
    Not in scope: ‘satQueryReason’
    Perhaps you want to add ‘satQueryReason’ to the import list
    in the import of ‘What4.Interface’
    (src/What4/Solver/ABC.hs:(81,1)-(82,95)).
    |
748 |     , satQueryReason = logReason logData
    |       ^^^^^^^^^^^^^^

src/What4/Solver/ABC.hs:794:9: error:
    Not in scope: ‘satQueryResult’
    Perhaps you want to add ‘satQueryResult’ to the import list
    in the import of ‘What4.Interface’
    (src/What4/Solver/ABC.hs:(81,1)-(82,95)).
    |
794 |       { satQueryResult = forgetModelAndCore res
    |         ^^^^^^^^^^^^^^

src/What4/Solver/ABC.hs:795:9: error:
    Not in scope: ‘satQueryError’
    Perhaps you want to add ‘satQueryError’ to the import list
    in the import of ‘What4.Interface’
    (src/What4/Solver/ABC.hs:(81,1)-(82,95)).
    |
795 |       , satQueryError  = Nothing
    |         ^^^^^^^^^^^^^

And on what4-blt:

[1 of 1] Compiling What4.Solver.BLT ( src/What4/Solver/BLT.hs, /home/rscott/Documents/Hacking/Haskell/what4-2/dist-newstyle/build/x86_64-linux/ghc-8.10.4/what4-blt-0.2/build/What4/Solver/BLT.o, /home/rscott/Documents/Hacking/Haskell/what4-2/dist-newstyle/build/x86_64-linux/ghc-8.10.4/what4-blt-0.2/build/What4/Solver/BLT.dyn_o )

src/What4/Solver/BLT.hs:135:5: error:
    • Constructor ‘SolverStartSATQuery’ does not have field ‘satQuerySolverName’
    • In the second argument of ‘logSolverEvent’, namely
        ‘SolverStartSATQuery
           {satQuerySolverName = "BLT", satQueryReason = logReason logData}’
      In a stmt of a 'do' block:
        logSolverEvent
          sym
          SolverStartSATQuery
            {satQuerySolverName = "BLT", satQueryReason = logReason logData}
      In the expression:
        do let cfg = getConfiguration sym
           epar <- parseBLTParams . T.unpack
                     <$> (getOpt =<< getOptionSetting bltParams cfg)
           par <- either fail return epar
           logSolverEvent
             sym
             SolverStartSATQuery
               {satQuerySolverName = "BLT", satQueryReason = logReason logData}
           ....
    |
135 |     SolverStartSATQuery
    |     ^^^^^^^^^^^^^^^^^^^...

src/What4/Solver/BLT.hs:135:5: error:
    • Constructor ‘SolverStartSATQuery’ does not have field ‘satQueryReason’
    • In the second argument of ‘logSolverEvent’, namely
        ‘SolverStartSATQuery
           {satQuerySolverName = "BLT", satQueryReason = logReason logData}’
      In a stmt of a 'do' block:
        logSolverEvent
          sym
          SolverStartSATQuery
            {satQuerySolverName = "BLT", satQueryReason = logReason logData}
      In the expression:
        do let cfg = getConfiguration sym
           epar <- parseBLTParams . T.unpack
                     <$> (getOpt =<< getOptionSetting bltParams cfg)
           par <- either fail return epar
           logSolverEvent
             sym
             SolverStartSATQuery
               {satQuerySolverName = "BLT", satQueryReason = logReason logData}
           ....
    |
135 |     SolverStartSATQuery
    |     ^^^^^^^^^^^^^^^^^^^...

src/What4/Solver/BLT.hs:143:7: error:
    • Constructor ‘SolverEndSATQuery’ does not have field ‘satQueryResult’
    • In the second argument of ‘logSolverEvent’, namely
        ‘SolverEndSATQuery
           {satQueryResult = forgetModelAndCore result,
            satQueryError = Nothing}’
      In a stmt of a 'do' block:
        logSolverEvent
          sym
          SolverEndSATQuery
            {satQueryResult = forgetModelAndCore result,
             satQueryError = Nothing}
      In the expression:
        do forM_ ps (assume h)
           result <- checkSat h
           logSolverEvent
             sym
             SolverEndSATQuery
               {satQueryResult = forgetModelAndCore result,
                satQueryError = Nothing}
           contFn result
    |
143 |       SolverEndSATQuery
    |       ^^^^^^^^^^^^^^^^^...

src/What4/Solver/BLT.hs:143:7: error:
    • Constructor ‘SolverEndSATQuery’ does not have field ‘satQueryError’
    • In the second argument of ‘logSolverEvent’, namely
        ‘SolverEndSATQuery
           {satQueryResult = forgetModelAndCore result,
            satQueryError = Nothing}’
      In a stmt of a 'do' block:
        logSolverEvent
          sym
          SolverEndSATQuery
            {satQueryResult = forgetModelAndCore result,
             satQueryError = Nothing}
      In the expression:
        do forM_ ps (assume h)
           result <- checkSat h
           logSolverEvent
             sym
             SolverEndSATQuery
               {satQueryResult = forgetModelAndCore result,
                satQueryError = Nothing}
           contFn result
    |
143 |       SolverEndSATQuery
    |       ^^^^^^^^^^^^^^^^^...

This is due to #111. Patch incoming.

We've been trying to convert a tool from using the sbv library to what4, which seems like a better fit for our work. Our one remaining issue involves manipulation of the entry stack. For example, from my experience with sbv, and my understanding of smtlib, I would have expected:

pushEntryStack w
assume w p
popEntryStack w

to always be a no-op. But it appears that the assumption of p remains on returning to the previous context.

So what is going on here, and how then would we use what4 to check satisfiabilty of a single predicate, within the current context, without infecting the global state?

There are still quite a few places here and there where we are using error or fail when we should instead replace those with panic or other more targeted error handling mechanisms instead.

Every time I compile what4 I get this warning from the build:

/Users/huffman/Work/saw-script/deps/what4/what4/src/What4/Protocol/SMTLib2/Parse.hs:491:44: error:
     warning: treating Unicode character <U+2217> as identifier character rather than as '*' symbol [-Wunicode-homoglyph]
    |
491 | -- | Parses ⟨symbol⟩ ( ⟨sorted_var⟩∗ ) ⟨sort⟩ ⟨term⟩
    |                                            ^
-- | Parses ⟨symbol⟩ ( ⟨sorted_var⟩∗ ) ⟨sort⟩ ⟨term⟩
                                   ^

I believe that this warning originates from the C preprocessor.

https://github.com/GaloisInc/crucible/blob/ce240b9703e999cf9a8c4e8e4c1855b423fd9207/what4/src/What4/Utils/AnnotatedMap.hs#L61-L62

I'm 100% sure, but it seems to me like this will sequence the effects in the Applicative from back-to-front rather than the more usual front-to-back order.

The mkIte function in what4 could implement additional simplifications for when one of the branches is another ite with the same condition.

https://github.com/GaloisInc/crucible/blob/943e47ddfe4fd2374c2aaa35c0d18f3576354741/what4/src/What4/Expr/Builder.hs#L3659-L3679

More specifically, the new rewrite rules would be

• ite c x (ite c y z) == ite c x z
• ite c (ite c x y) z == ite c x z

Now that what4 is changed to use prettyprinter output with the ability to annotate pretty-printed elements, it may be useful to create a concrete annotation type to identify the element type for rendering-time formatting (see #77 (comment)).

Can you please make it clear with the license is? Hackage says the license is BSD-3-Clause, that the license is not obvious when looking at this GitHub repository. Maybe simply put the license text of BSD-3-Clause into a file named LICENSE ?

Thanks!

While adding QuickCheck properties to the BVDomain code, mirroring the Cryptol properties in the specification, I discovered that sdiv and srem do not meet their specs.

From the Cryptol specification:

arithdomain> :set base=10
arithdomain> let a = interval`{6} 6 9
arithdomain> let b = interval`{6} 36 33
arithdomain> a
{lo = 6, sz = 9}
arithdomain> b
{lo = 36, sz = 33}
arithdomain> sdiv a b
{lo = 49, sz = 30}

From the Haskell:

> let a = range (knownNat :: NatRepr 6) 6 (6+9)
> let b = range (knownNat :: NatRepr 6) 36 (36+33)
> a
BVDInterval 63 6 9
> b
BVDInterval 63 36 33
> sdiv (knownNat :: NatRepr 6) a b
BVDInterval 63 0 3

There are counterexamples for srem as well, but I haven't found any this small. I'm guessing the bugs are related, and have something to do with emulating bitvectors using integers; but it isn't obvious.

@brianhuffman, any ideas?

When I create a struct with a single Nat field, the constraint that the field is positive does not get output to the solver. I only found this because it resulted in an arithmetic underflow in certain cases.

See https://gist.github.com/benjaminselfridge/b55319660c6dd0609f1c17329abc4cb8

Currently, we cannot parse the models for uninterepted functions and arrays from solvers. Because there is no SMTLib2 standard for this, each solver does it a little differently.

For some of my purposes in building a Sally programs from Crucible programs, I am trying to use What4 as a glorified pretty-printer (with minimal solving involved). Unfortunately, the Sally syntax requires me to do non-SMTLib2-compliant operations to the produced expressions.

Given the current infrastructure of SMTWriter, I got to a working solution by exposing the following symbols:

CollectorResults(..)
mkBaseExpr
runInSandbox
typeMap

The first three let me build my own writer, and intercept the collector results, as I process them in a ad hoc way.

The latter I'm using to get from a What4.BaseTypeRepr to a SMT2.Sort, and am wondering whether I am missing a helper to do so.

Would these be okay to expose?
Eventually, I have larger ideas on how to reformulate SMTWriter to allow for the flexibility I need without "leaking" the aforementioned functions, but in the meantime, this is currently working well for me.

  Z3 string4:                              FAIL (0.13s)
    test/ExprBuilderSMTLib2.hs:794:
    substring not found
...
1 out of 54 tests failed (4.27s)
Test suite expr-builder-smtlib2: FAIL

All other tests pass. With Z3 4.8.8 and everything else unchanged the tests pass.

When 4.0 was released, it included a breaking change to a constructor. We fixed that by adding an upper version bound on the package in our cabal file. We should adapt to the new API and update the bound to >=4 && <4.1 at some point, to make sure we don't get pinned to some older versions of other dependencies

It would be more convenient for many clients of what4 if there was a single solver timeout option that would propagate to any solver that supported it (and maybe lead to a warning for solvers that don't support it?). Currently, each solver has its own option.

When attempting to declare a fresh constant multi-dimensional array, the Z3 backend is not correctly declaring the Struct2 type needed to index into the array.

(declare-fun x!5 () (Array (Struct2 Int (_ BitVec 64)) (_ BitVec 8)))
; (error "line 22 column 29: unknown sort 'Struct2'")

Full log: solver2.log

If a redundant term that has the expected struct type is explicitly declared and used, then the backend correctly declares the expected datatype and the array declaration is valid. However, for reasons unknown, Z3 occasionally throws an error saying that the constructor mk-struct2 has already been declared, but at the point where the type is used.

(declare-datatypes (T0 T1) ((Struct2 (mk-struct2 (struct2-proj0 T0) (struct2-proj1 T1)))))
...
(define-fun x!740 () (Array (Struct2 Int (_ BitVec 64)) (_ BitVec 8)) (store x!20 (mk-struct2 1 x!738) x!739))
; (error "line 843 column 54: invalid declaration, function 'mk-struct2' (with the given signature) already declared")

Full log : solver.log

Z3 version: 4.8.6 - Mac OS X 10.14

Consider the freshBoundedBV, freshBoundedInt, etc. operations of the what4 interface. At the moment, these are implement simply by adding abstract domain information to the uninterpreted constant values. This means that, when traversing terms to export them to SMT or other backends, the traversal must pay special attention to the abstract domain information for constants and emit corresponding assumptions to avoid finding spurious models. This is not obvious and rather error prone. For example, the SAWCore backend ignores the abstract domain information. This is OK, but only because SAW doesn't use the bounded methods.

It would be better to have a special term constructor that attaches side conditions to terms instead. Then, it will be obvious during term traversals where additional assumptions must be recorded, making the process less error prone. The same mechanism could also be used for more general types of assumptions (e.g., uniquely specifying a value instead of computing it).

Now that we've reworked how weighed sums work, I think we can revisit enabling abstract domain calculations for bitwise operations. In addition, we should investigate if it makes sense to implement domain calculations for popcount, ctz, and clz, rol, and ror.

The docs for freshBoundedInt etc. don't make it clear which argument is the upper bound and which the lower. Lower being first is indeed more intuitive, but the docs say upper and lower, which introduces enough doubt that I had to actually run some tests to verify this.

The current Verilog generation backend produces Verilog like the following:

output [31:0] out = wr_5;

According to @rtadros125, this isn't considered good form. Instead, we should do something like:

output [31:0] out;
assign out = wr_5;

ABC seems to accept the latter form, so we should probably modify the generator to produce it.

CF:

I'm pretty confident this implementation of testBit is incorrect. Consider a domain on 8-bit values with a low bound at 0xFF and wraps around 0 all the way to to 0xF0. According to this testBit implementation, all the high bits in this range will be considered constant 1, even though they pass through all the values from 0x00 to 0xF0.

A correct implementation should use the unknowns function, which properly accounts for this wraparound behavior.

As I understand it, boolector does not currently allow you to set per-goal timeouts. Let's see if we can convince the boolector devs to add a relevant timeout option and hook it up.

Min/max for integers and reals can be defined using comparisons and if/then/else, but there are advantages to defining them as primitives. We can directly encode idempotent laws and provide better abstract domain information by making them primitive.

Right now, we represent the concrete values of bitvectors in what4 simply as Haskell Integers, with the convention that values are always truncated to the correct number of bits. This is a bit error-prone, and it turns out that the process of defensively masking integers to the correct number of bits has nontrivial performance implications.

We should transition to a datatype for bitvectors that abstracts over the concrete representation so that we can increase our confidence that they our computations are being done correctly, and so that we can experiment with alternate implementation strategies.

https://github.com/GaloisInc/bv-sized is probably a good start for what we need.

If useSymbolicArrays is turned on, What4 will still back a constant array with a lambda function, which can generate invalid yices input:

e.g. updating a constant array with symbolic values and then making assertions about the contents yields
the following yices program

(define x!1::(bitvector 64))
(define x!5::(bitvector 64))

(define x!2::(-> int (bitvector 64) bool) (lambda (i!5::int i!6::(bitvector 64)) false))
(define x!3::(-> int (bitvector 64) bool) (update x!2 (0 x!1) true))
(define x!4::bool (x!3 0 x!5))
(assert x!4)

Which then crashes with the output:

the context does not support lambdas (line 7, column 13)

In support for GaloisInc/crucible#414, it would be useful to have a general library for doing sharing-aware traversals of What4 expressions. A sharing-aware pretty-printing library could be built on top of such a traversal, but many other forms of traversal could benefit from being able to share some of the memo table boilerplate.

Z3 and CVC4 have diverged recently on their encoding of string literal values.

CVC4 (as of 1.9-prerelease [git master e8482734], and probably released 1.8, I need to check) now appears to be following the (draft?) SMTLib2 Unicode conventions for escaping (http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml), where escape codes have a leading \u. I need to find out if they have also changed their string theory to be unicode-based.

Meanwhile, Z3 seems to still be using their home-grown escaping system for ASCII using \x00 style escapes (as of Z3 4.8.7).

Previously, CVC4 used the same system as Z3. Now, we get different results from problems that go outside the non-printable ASCII range.

The haddock documentation for What4.Interface.intDiv says that it satisfies the spec x * (div x y) + (mod x y) == x. This should instead say that y * (div x y) + (mod x y) == x.

The statement "The value of @intDiv x y@ is undefined when @y = 0@" could also use more explanation. What kind of undefinedness is this? I believe it means that the function doesn't cause an error or an exception when y = 0, just that its return value is unspecified/undetermined.

The same docstring has an ill-formatted bulleted list at the end; we should fix this as well.

This would be useful as a quick check to see if we can find the appropriate solver binaries and perform the minimum required interaction to issue queries and return results.

When solvers terminate with a timeout or other indeterminate result, it would be nice to provide additional information (ultimately provided by the solver) back to the client. A starting point could be to return a string containing all extra output produceed by the solver.

CF GaloisInc/saw-script#1166

%< ---------------------------------------------------
Revision: 8402ae2
Branch: HEAD
Location: bvSliceBE
Message: invalid arguments to slice: 128 0 from vector of length 128
CallStack (from HasCallStack):
panic, called at src/What4/Panic.hs:17:9 in what4-1.0.0.0.99-inplace:What4.Panic
panic, called at src/What4/SWord.hs:325:5 in what4-1.0.0.0.99-inplace:What4.SWord
%< ---------------------------------------------------

A slice of 0 bits is rejected by the SWord module with a panic, but it should probably just be accepted instead and return the distinguished ZBV value instead.