diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-04-24 18:36:40 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-04-24 18:36:40 +0000 |
| commit | c0f5194dd56c5127c5c6dab5e59997eccc2d78a5 (patch) | |
| tree | 080d465b923832f14d67da4431642609d66b921b /test | |
| parent | 5676b8bddcf001ba567ebb6d8e7b42dbd13ac9f3 (diff) | |
This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:
- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/uflra/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/constants0.smt | 15 |
2 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 4817582c0..0418fc3e9 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -13,6 +13,7 @@ MAKEFLAGS = -k # Regression tests for SMT inputs SMT_TESTS = \ + constants0.smt \ simple.01.cvc \ simple.02.cvc \ simple.03.cvc \ diff --git a/test/regress/regress0/uflra/constants0.smt b/test/regress/regress0/uflra/constants0.smt new file mode 100644 index 000000000..b07a6bc4e --- /dev/null +++ b/test/regress/regress0/uflra/constants0.smt @@ -0,0 +1,15 @@ +(benchmark mathsat +:logic QF_UFLRA +:status unsat +:category { crafted } +:extrafuns ((f Real Real)) +:extrafuns ((x Real)) +:extrafuns ((y Real)) +:formula +(and (or (= x 3) (= x 5)) + (or (= y 3) (= y 5)) + (not (= (f x) (f y))) + (implies (= (f 3) (f x)) (= (f 5) (f x))) + (implies (= (f 3) (f y)) (= (f 5) (f y))) +) +)
\ No newline at end of file |