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

more regression tests

Browse source
This commit is contained in:
Simon Cruanes 2020-12-22 15:02:12 -05:00
parent 7ef673ca30
commit 23dcf79560
3 changed files with 255 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

203
tests/sat/uart-10.induction.cvc.smt2 Normal file
View file

File diff suppressed because one or more lines are too long

36
tests/unsat/reg_lra_fm1.smt2 Normal file
View file

@ -0,0 +1,36 @@
; expect: unsat
; intermediate problem in tests/unsat/clocksynchro_2clocks.worst_case_skew.base.smt2
(set-logic QF_LRA)
(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 (< (+ (/ 2335 666) x_5 x_6 (* (/ 2 999) x_7) (* (/ 2 999) x_4)) 0))
(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_2) 0))
(assert (<= (+ (/ 999 1000) x_0 (* -1 x_2)) 0))
(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_1) 0))
(assert (<= (+ (/ 999 1000) x_0 (- 0 x_1)) 0))
(assert (= x_0 0))
(assert
(<= (+
(/ 1502501 999000)
(* (/ 1001 999) x_5)
(* (/ 1001 999) x_6)
(* -1 x_7)
(* (/ 1001 999) x_3))
0))
(assert (< (+ (/ 1001 2) (* (/ 999 2) x_6) x_7 (* (/ -999 2) x_4)) 0))
(assert (<= (+ (/ 1001 999) x_5 (* -1 x_6) (* (/ 1001 1998) x_4)) 0))
(assert (< (* -1 x_5) 0))
(assert (< (* -1 x_4) 0))
(assert (< (* -1 x_3) 0))
(check-sat)

16
tests/unsat/smtlib.624916.smt2 Normal file
View file

@ -0,0 +1,16 @@
(set-info :smt-lib-version 2.6)
(set-logic QF_UFLRA)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-sort S1 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (Real) Real)
(declare-fun f4 () Real)
(declare-fun f5 () Real)
(assert (not (= f1 f2)))
(assert (= (f3 f4) (- 1)))
(assert (not (=> (= f5 f4) (not (= (f3 f5) 1.0)))))
(check-sat)
(exit)