From 82f4d5bd67f70a561b0f6357f6d6b80c2fcd7b64 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 21 Apr 2015 16:34:56 +0200 Subject: Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions. --- test/regress/regress0/datatypes/Makefile.am | 4 +- test/regress/regress0/datatypes/bug625.smt2 | 13 +++++ test/regress/regress0/datatypes/manos-model.smt2 | 67 ++++++++++++++++++++++++ 3 files changed, 83 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/datatypes/bug625.smt2 create mode 100644 test/regress/regress0/datatypes/manos-model.smt2 (limited to 'test/regress/regress0') diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index b323a2732..45060dbd3 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -63,7 +63,9 @@ TESTS = \ tenum-bug.smt2 \ cdt-non-canon-stream.smt2 \ stream-singleton.smt2 \ - is_test.smt2 + is_test.smt2 \ + manos-model.smt2 \ + bug625.smt2 FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/bug625.smt2 b/test/regress/regress0/datatypes/bug625.smt2 new file mode 100644 index 000000000..3f4312ad4 --- /dev/null +++ b/test/regress/regress0/datatypes/bug625.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun y1 () Int) +(declare-fun y2 () Int) +(declare-datatypes () ( (type + (constructor1 (f1 Int)) + (constructor2 (f2 Int)) +))) +(define-fun mktest ((constructor Int) (p1 Int) (p2 Int)) type (ite (= constructor 1) (constructor1 p1) (constructor2 p2))) +(assert (distinct (mktest x1 x2 x2) (mktest y1 y2 y2))) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress0/datatypes/manos-model.smt2 b/test/regress/regress0/datatypes/manos-model.smt2 new file mode 100644 index 000000000..4ade71151 --- /dev/null +++ b/test/regress/regress0/datatypes/manos-model.smt2 @@ -0,0 +1,67 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ( (tuple2!879 (tuple2!879!880 (_1!881 Int) (_2!882 Int))) )) + +(declare-fun p1!207 () tuple2!879) + +(declare-fun p2!208 () tuple2!879) + +(declare-fun p3!209 () tuple2!879) + +(declare-fun reduce!206 (tuple2!879 tuple2!879) tuple2!879) + +(assert (not (= + (reduce!206 p1!207 (reduce!206 p2!208 p3!209)) + (reduce!206 (reduce!206 p1!207 p2!208) p3!209) +))) + +(assert (= + (reduce!206 p1!207 (reduce!206 p2!208 p3!209)) + (ite + (>= (_1!881 p1!207) (_2!882 (reduce!206 p2!208 p3!209))) + (tuple2!879!880 + (+ (- (_1!881 p1!207) (_2!882 (reduce!206 p2!208 p3!209))) (_1!881 (reduce!206 p2!208 p3!209))) + (_2!882 p1!207) + ) + (tuple2!879!880 + (_1!881 (reduce!206 p2!208 p3!209)) + (+ (- (_2!882 (reduce!206 p2!208 p3!209)) (_1!881 p1!207)) (_2!882 p1!207)) + ) + ) +)) + +(assert (= + (reduce!206 p2!208 p3!209) + (ite + (>= (_1!881 p2!208) (_2!882 p3!209)) + (tuple2!879!880 (+ (- (_1!881 p2!208) (_2!882 p3!209)) (_1!881 p3!209)) (_2!882 p2!208)) + (tuple2!879!880 (_1!881 p3!209) (+ (- (_2!882 p3!209) (_1!881 p2!208)) (_2!882 p2!208))) + ) +)) + +(assert (= + (reduce!206 (reduce!206 p1!207 p2!208) p3!209) + (ite + (>= (_1!881 (reduce!206 p1!207 p2!208)) (_2!882 p3!209)) + (tuple2!879!880 + (+ (- (_1!881 (reduce!206 p1!207 p2!208)) (_2!882 p3!209)) (_1!881 p3!209)) + (_2!882 (reduce!206 p1!207 p2!208)) + ) + (tuple2!879!880 + (_1!881 p3!209) + (+ (- (_2!882 p3!209) (_1!881 (reduce!206 p1!207 p2!208))) (_2!882 (reduce!206 p1!207 p2!208))) + ) + ) +)) + +(assert (= + (reduce!206 p1!207 p2!208) + (ite + (>= (_1!881 p1!207) (_2!882 p2!208)) + (tuple2!879!880 (+ (- (_1!881 p1!207) (_2!882 p2!208)) (_1!881 p2!208)) (_2!882 p1!207)) + (tuple2!879!880 (_1!881 p2!208) (+ (- (_2!882 p2!208) (_1!881 p1!207)) (_2!882 p1!207))) + ) +)) + +(check-sat) + -- cgit v1.2.3