diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-01 15:10:23 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-01 13:10:23 -0700 |
| commit | b0fd7761fc36fc53141cb1486e9cb19dd00ae5f3 (patch) | |
| tree | 56da6668e0d328943b9a4906b49bafca2aed7c83 /test/regress/regress0/quantifiers | |
| parent | 4be329c881c510caab5995b5ecbe3ae9961b3eed (diff) | |
Use monomial sum utility to solve for quantifiers macros (#2038)
Diffstat (limited to 'test/regress/regress0/quantifiers')
| -rw-r--r-- | test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
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) |