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

add regression tests for LRA

Browse source
This commit is contained in:
Simon Cruanes 2020-10-20 15:43:02 -04:00
parent f556fe58ab
commit f510bfaf25
5 changed files with 6718 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
Makefile
View file

@ -41,6 +41,9 @@ $(TESTTOOL)-smt-QF_UF: snapshots
$(TESTTOOL)-smt-QF_DT: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/smt-QF_DT-$(DATE).csv --task sidekick-smt-nodir tests/QF_DT
$(TESTTOOL)-smt-QF_LRA: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/smt-QF_LRA-$(DATE).csv --task sidekick-smt-nodir tests/QF_LRA
install: build-install
@dune install

537
tests/sat/broydn.c.i.broydn.pl.t2.fixed.t2.c_Iteration8_Loop_7-phaseTemplate.smt2 Normal file
View file

File diff suppressed because one or more lines are too long

6135
tests/sat/disj_nightmare.t2.c_Iteration1_Loop_3-pieceTemplate.smt2 Normal file
View file

File diff suppressed because one or more lines are too long

16
tests/unsat/clocksynchro_2clocks.worst_case_skew.base.smt2 Normal file
View file

@ -0,0 +1,16 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_LRA)
(set-info :source | Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(assert (let ((?v_0 (+ x_0 (/ 999 1000))) (?v_1 (+ x_0 (/ 1001 1000))) (?v_2 (not (<= (- 1 1) (+ (+ (+ x_5 x_6) (* (* (+ x_7 x_4) 2) (/ 1 999))) (/ 2335 666)))))) (and (and (and (and (and (and (and (and (and (and (and (not (<= x_3 0)) (not (<= x_4 0))) (not (<= x_5 0))) (not (< x_6 (+ x_5 (* (* (+ (* (* x_4 1) (/ 1 2)) 1) 1001) (/ 1 999)))))) (< x_7 (- (* (* (- (- x_4 x_6) 1) 999) (/ 1 2)) 1))) (not (< x_7 (* (* (+ (+ (+ x_3 x_5) x_6) (/ 1501 1000)) 1001) (/ 1 999))))) (= x_0 0)) (<= ?v_0 x_1)) (<= x_1 ?v_1)) (<= ?v_0 x_2)) (<= x_2 ?v_1)) (or (or (or ?v_2 ?v_2) ?v_2) ?v_2))))
(check-sat)
(exit)

27
tests/unsat/simple_example_1-node2318.smt2 Normal file
View file

@ -0,0 +1,27 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_LRA)
(set-info :source |
These benchmarks used in the paper:
Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic.
In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
The keymaera family contains VCs from Keymaera verification, see:
A. Platzer, J.-D. Quesel, and P. Rummer. Real world verification.
In CADE 2009, pages 485-501. Springer, 2009.
Submitted by Dejan Jovanovic for SMT-LIB.
KeYmaera example: simple_example_1, node 2318 For more info see: No further information available.
|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun e () Real)
(declare-fun buscore2dollarskuscore1 () Real)
(declare-fun duscore2dollarskuscore1 () Real)
(declare-fun cuscore2dollarskuscore1 () Real)
(declare-fun auscore2dollarskuscore1 () Real)
(assert (not (=> (and (and (= e 0) (= (* 2 auscore2dollarskuscore1) buscore2dollarskuscore1)) (= cuscore2dollarskuscore1 duscore2dollarskuscore1)) (= (+ cuscore2dollarskuscore1 1) (+ duscore2dollarskuscore1 1)))))
(check-sat)
(exit)