Skip to content

Commit

Permalink
Update CVC5 tested date and match new output from CVC5
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed Nov 30, 2023
1 parent 9240646 commit d780fed
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 6 deletions.
8 changes: 4 additions & 4 deletions Documentation/SBV/Examples/Queries/Abducts.hs
Original file line number Diff line number Diff line change
Expand Up @@ -22,10 +22,10 @@ import Data.SBV.Control
-- and we want to make @x + y >= 2@. We have:
--
-- >>> example
-- Got: (define-fun abd () Bool (= s1 2))
-- Got: (define-fun abd () Bool (<= 2 s1))
-- Got: (define-fun abd () Bool (= (+ s1 s0) 2))
-- Got: (define-fun abd () Bool (= (+ s0 2) s1))
-- Got: (define-fun abd () Bool (and (= s0 s1) (= s0 1)))
-- Got: (define-fun abd () Bool (and (= 2 s1) (= s0 1)))
-- Got: (define-fun abd () Bool (and (= s0 s1) (<= 1 s1)))
-- Got: (define-fun abd () Bool (= 2 s1))
--
-- Note that @s0@ refers to @x@ and @s1@ refers to @y@ above. You can verify
-- that adding any of these will ensure @x + y >= 2@.
Expand Down
4 changes: 2 additions & 2 deletions SMTSolverVersions.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ report any issues you might see with newer releases.
on Jul 27, 2020.
* CVC5:
* https://github.com/cvc5/cvc5
* Version 1.0.5, downloaded compiled from GitHub repo above on Mar 13th, 2023.
* Version 1.0.8, downloaded compiled from GitHub repo above on Nov 29th, 2023.
* dReal:
* http://dreal.github.io/
* Version installed via `brew tap dreal/dreal; brew rm dreal; brew install dreal --HEAD`
Expand All @@ -33,7 +33,7 @@ report any issues you might see with newer releases.
* Version 2.6.2 as downloaded from the above site on Apr 7, 2020
* Z3:
* http://github.com/Z3Prover/z3
* Version as downloaded from the above site on Oct 29th, 2023
* Version as downloaded from the above site on Nov 29th, 2023
* SBV typically relies on latest features of z3, so compiling directly
from the sources is recommended. If that's not possible, you should
always use their latest release.

0 comments on commit d780fed

Please sign in to comment.