github-mig/ZoKrates
github-mig/ZoKrates
1
0
Fork 0
mirror of synced 2025-09-24 04:40:05 +00:00
Code Issues Projects Releases Wiki Activity

fix smt test

Browse source
This commit is contained in:
schaeff 2021-12-08 15:03:31 +01:00
parent 0626ca4297
commit 0877800cef
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
zokrates_cli/tests/code/taxation.smt2
View file

@ -261,7 +261,7 @@
(declare-const |_254| Int)
(declare-const |_257| Int)
(declare-const |_258| Int)
(declare-const |_263| Int)
(declare-const |_264| Int)
(assert (and
(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
(= |~one| 1)
@ -524,6 +524,6 @@
(= (mod (* (+ (* |~one| 14651237294507013008273219182214280847718990358813499091232105186081237893121) (* |_0| 1) (* |_1| 21888242871839275222246405745257275088548364400416034343698204186575808495616)) (* |_258| 1)) |~prime|) (mod (* |_257| 1) |~prime|))
(= (mod (* (+ (* |~one| 1) (* |_257| 21888242871839275222246405745257275088548364400416034343698204186575808495616)) (+ (* |~one| 14651237294507013008273219182214280847718990358813499091232105186081237893121) (* |_0| 1) (* |_1| 21888242871839275222246405745257275088548364400416034343698204186575808495616))) |~prime|) (mod 0 |~prime|))
(= (mod (* (* |~one| 1) 0) |~prime|) (mod (+ (* |~one| 1) (* |_257| 21888242871839275222246405745257275088548364400416034343698204186575808495616)) |~prime|))
(= (mod (* (* |_2| 1) (+ (* |_0| 21888242871839275222246405745257275088548364400416034343698204186575808495616) (* |_1| 1))) |~prime|) (mod (* |_263| 1) |~prime|))
(= (mod (* (* |~one| 1) (* |_263| 1)) |~prime|) (mod (* |~out_0| 1) |~prime|))
(= (mod (* (* |_2| 1) (+ (* |_0| 21888242871839275222246405745257275088548364400416034343698204186575808495616) (* |_1| 1))) |~prime|) (mod (* |_264| 1) |~prime|))
(= (mod (* (* |~one| 1) (* |_264| 1)) |~prime|) (mod (* |~out_0| 1) |~prime|))
))