simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

update tests

Browse source
This commit is contained in:
Simon Cruanes 2022-07-14 21:48:19 -04:00
parent b16fce6f26
commit 96bc3e2340
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/guide.md
View file

@ -347,9 +347,7 @@ Sidekick_base_solver.Solver.Sat
(a := 0) (a := 0)
(b := 0) (b := 0)
((<= (+ a (* -1 b)) 0) := true) ((<= (+ a (* -1 b)) 0) := true)
(_sk_lra__le_comb0 := 0) (_sk_lra__le_comb0 := 0))
((= a b) := true)
((>= (+ a (* -1 b)) 0) := true))
# let a_geq_1 = Term.LRA.(geq tstore a (const tstore (Q.of_int 1)));; # let a_geq_1 = Term.LRA.(geq tstore a (const tstore (Q.of_int 1)));;

4
src/tests/regression/reg_model_lra1.out.expected
View file

@ -2,8 +2,8 @@
(true := true) (true := true)
(false := false) (false := false)
(a := 5/3) (a := 5/3)
((* 3 a) := 5) ((* 3 a) := 0)
(5 := 5) (5 := 0)
((= (* 3 a) 5) := true) ((= (* 3 a) 5) := true)
((<= (* 3 a) 5) := true) ((<= (* 3 a) 5) := true)
((>= (* 3 a) 5) := true)) ((>= (* 3 a) 5) := true))