From 86eedb9ce9d4ea399997fd6fbdfe41f99ac22453 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 17 Oct 2018 22:24:02 -0700 Subject: [PATCH] Skip sygus-rr-synth-check regressions when ASAN on (#2651) This commit disables three regressions when using an ASAN build. The regressions are all leaking memory when invoking the subsolver (see issue #2649). Debugging the issue will take a while but is not very critical since this feature is currently only used by CVC4 developers but it prevents our nightly builds from going through. --- test/regress/regress1/rr-verify/bv-term.sy | 1 + test/regress/regress1/rr-verify/fp-arith.sy | 1 + test/regress/regress1/rr-verify/fp-bool.sy | 1 + 3 files changed, 3 insertions(+) diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy index f310396d2..278c10339 100644 --- a/test/regress/regress1/rr-verify/bv-term.sy +++ b/test/regress/regress1/rr-verify/bv-term.sy @@ -1,3 +1,4 @@ +; REQUIRES: no-asan ; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break ; COMMAND-LINE: --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy index cca2487d4..61dc19fbb 100644 --- a/test/regress/regress1/rr-verify/fp-arith.sy +++ b/test/regress/regress1/rr-verify/fp-arith.sy @@ -1,3 +1,4 @@ +; REQUIRES: no-asan ; REQUIRES: symfpu ; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy index 8792a594c..8e404668e 100644 --- a/test/regress/regress1/rr-verify/fp-bool.sy +++ b/test/regress/regress1/rr-verify/fp-bool.sy @@ -1,3 +1,4 @@ +; REQUIRES: no-asan ; REQUIRES: symfpu ; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.") -- 2.30.2