mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-10-26 14:20:59 +03:00
Make issue{066,093} resilient to different solvers' behavior
This adopts the same approach as in commit
3ea5e9e51c
:
use `:set show-examples=false` in the affected examples to avoid showing the
particular data that a solver picks for examples/counterexamples. Also avoid
printing the contents of `it` for similar reasons. I have verified that the
new output works across a wide range of Z3 versions.
Fixes #1280.
This commit is contained in:
parent
3a204fc4aa
commit
09aaf1d82c
@ -1,35 +1,27 @@
|
||||
// Don't show examples, as they can differ depending on the solver version.
|
||||
// See #1280.
|
||||
:set show-examples=false
|
||||
let f x = (x : [4]) == x
|
||||
:prove f
|
||||
:t it
|
||||
it
|
||||
it.result
|
||||
let f x = (x : [4]) == 3
|
||||
:prove f
|
||||
:t it
|
||||
it
|
||||
it.result
|
||||
:sat f
|
||||
:t it
|
||||
it
|
||||
it.result
|
||||
let f x = (x : [4]) == 3 /\ x == 2
|
||||
:sat f
|
||||
:t it
|
||||
it
|
||||
let g p = (p : { x : [32], y : [32]}).x == p.y
|
||||
:prove g
|
||||
:t it
|
||||
it
|
||||
:sat g
|
||||
:t it
|
||||
it
|
||||
let h x y = (x : [8]) < y
|
||||
:prove h
|
||||
:t it
|
||||
it
|
||||
let result = it
|
||||
result.arg1
|
||||
result.arg2
|
||||
:sat h
|
||||
:t it
|
||||
it
|
@ -1,42 +1,20 @@
|
||||
Loading module Cryptol
|
||||
Q.E.D.
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
|
||||
Run-time error: no counterexample available
|
||||
-- Backtrace --
|
||||
Cryptol::error called at issue066.icry:2:8--2:9
|
||||
True
|
||||
Counterexample
|
||||
f 0xc = False
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
{result = False, arg1 = 0xc}
|
||||
False
|
||||
Satisfiable
|
||||
f 0x3 = True
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
{result = True, arg1 = 0x3}
|
||||
True
|
||||
Unsatisfiable
|
||||
it : {result : Bit, arg1 : [4]}
|
||||
|
||||
Run-time error: no satisfying assignment available
|
||||
-- Backtrace --
|
||||
Cryptol::error called at issue066.icry:16:6--16:7
|
||||
Counterexample
|
||||
g {x = 0xffffffff, y = 0x00000000} = False
|
||||
it : {result : Bit, arg1 : {x : [32], y : [32]}}
|
||||
{result = False, arg1 = {x = 0xffffffff, y = 0x00000000}}
|
||||
Satisfiable
|
||||
g {x = 0x00000000, y = 0x00000000} = True
|
||||
it : {result : Bit, arg1 : {x : [32], y : [32]}}
|
||||
{result = True, arg1 = {x = 0x00000000, y = 0x00000000}}
|
||||
Counterexample
|
||||
h 0x00 0x00 = False
|
||||
it : {result : Bit, arg1 : [8], arg2 : [8]}
|
||||
{result = False, arg1 = 0x00, arg2 = 0x00}
|
||||
0x00
|
||||
0x00
|
||||
Satisfiable
|
||||
h 0x00 0x01 = True
|
||||
it : {result : Bit, arg1 : [8], arg2 : [8]}
|
||||
{result = True, arg1 = 0x00, arg2 = 0x01}
|
||||
|
@ -1,3 +1,5 @@
|
||||
// Don't show examples, as they can differ depending on the solver version.
|
||||
// See #1280.
|
||||
:set show-examples=false
|
||||
:sat \x -> x > 0x4
|
||||
:t it
|
||||
|
@ -1,4 +1,7 @@
|
||||
// Don't show examples, as they can differ depending on the solver version.
|
||||
// See #1280.
|
||||
:set show-examples=false
|
||||
:l issue093.cry
|
||||
:check
|
||||
:prove
|
||||
:sat
|
||||
:sat
|
||||
|
@ -12,7 +12,6 @@ Testing... Passed 100 tests.
|
||||
Expected test coverage: 0.00% (100 of 2^^64 values)
|
||||
property f0 Using exhaustive testing.
|
||||
Testing... Counterexample
|
||||
f0 = False
|
||||
:prove t0
|
||||
Q.E.D.
|
||||
:prove t1
|
||||
@ -21,15 +20,11 @@ f0 = False
|
||||
Q.E.D.
|
||||
:prove f0
|
||||
Counterexample
|
||||
f0 = False
|
||||
:sat t0
|
||||
Satisfiable
|
||||
t0 = True
|
||||
:sat t1
|
||||
Satisfiable
|
||||
t1 0x00000000 = True
|
||||
:sat t2
|
||||
Satisfiable
|
||||
t2 0xfffffffe 0xffffffff = True
|
||||
:sat f0
|
||||
Unsatisfiable
|
||||
|
Loading…
Reference in New Issue
Block a user