From b0fd7761fc36fc53141cb1486e9cb19dd00ae5f3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 1 Jun 2018 15:10:23 -0500 Subject: Use monomial sum utility to solve for quantifiers macros (#2038) --- test/regress/Makefile.tests | 1 + test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 | 10 ++++++++++ 2 files changed, 11 insertions(+) create mode 100644 test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 (limited to 'test') diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index b92acab94..72bb8e1d1 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -604,6 +604,7 @@ REG0_TESTS = \ regress0/quantifiers/lra-triv-gn.smt2 \ regress0/quantifiers/macros-int-real.smt2 \ regress0/quantifiers/macros-real-arg.smt2 \ + regress0/quantifiers/issue2033-macro-arith.smt2 \ regress0/quantifiers/matching-lia-1arg.smt2 \ regress0/quantifiers/mix-complete-strat.smt2 \ regress0/quantifiers/mix-match.smt2 \ diff --git a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 new file mode 100644 index 000000000..7993910fd --- /dev/null +++ b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --macros-quant +; EXPECT: sat +(set-logic AUFNIRA) +(set-info :status sat) +(declare-fun _substvar_4_ () Real) +(declare-sort S2 0) +(declare-sort S10 0) +(declare-fun f22 (S10 S2) Real) +(assert (forall ((?v0 S10) (?v1 S2)) (= _substvar_4_ (- (f22 ?v0 ?v1))))) +(check-sat) -- cgit v1.2.3