GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2025-01-05 23:17:42 +03:00
Code Issues Projects Releases Wiki Activity

Just a different example.

Browse Source 
This used to work with Z3 4.7.1 but does not with 4.8.4
This commit is contained in:
Iavor Diatchki 2019-01-09 11:26:53 -08:00
parent 454dd58fbd
commit f0e9dcf471
1 changed files with 23 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
lib/CryptolTC.z3
View File

@ -328,9 +328,27 @@
; ---
; (declare-fun kv0 () InfNat )
; (assert (cryVar kv0 ) )
; (assert (not (isFin kv0)))
; (assert (ite (isFin kv0) (>= (value kv0) 5) true))
; (check-sat )
; (declare-fun L () InfNat)
; (declare-fun w () InfNat)
;
; (assert (cryVar L))
; (assert (cryVar w))
;
; (assert (cryAssume (cryFin w)))
; (assert (cryAssume (cryGeq w (cryNat 1))))
; (assert (cryAssume (cryGeq (cryMul (cryNat 2) w) (cryWidth L))))
;
; (assert (cryProve
; (cryGeq
; (cryMul
; (cryCeilDiv
; (cryAdd (cryNat 1) (cryAdd L (cryMul (cryNat 2) w)))
; (cryMul (cryNat 16) w))
; (cryMul (cryNat 16) w))
; (cryAdd (cryNat 1) (cryAdd L (cryMul (cryNat 2) w))))))
;
; (check-sat)