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

test: regressions test for LRA

Browse source
This commit is contained in:
Simon Cruanes 2022-02-08 13:45:26 -05:00
parent e481c74398
commit 73289d1ded
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 21 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
tests/unsat/reg_lra_3.smt2 Normal file
View file

@ -0,0 +1,9 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_UFLRA)
(set-info :source |modified from smtlib.626179.smt2|)
(set-info :status unsat)
(declare-fun f3 () Real)
(declare-fun f4 () Real)
(assert (not (=> (< f3 f4) (=> (< f4 (* 2.0 f3)) (< 0.0 (- f4 f3))))))
(check-sat)
(exit)

12
tests/unsat/reg_lra_4.smt2 Normal file
View file

@ -0,0 +1,12 @@
(set-logic QF_LRA)
(set-info :status unsat)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun p1 () Bool)
(declare-fun p2 () Bool)
(assert (<= a b))
(assert (= p1 (>= a 1)))
(assert (= p2 (<= b (/ 1 2))))
(check-sat-assuming (p1 p2))
(exit)