Skip sygus-rr-synth-check regressions when ASAN on (#2651)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 18 Oct 2018 05:24:02 +0000 (22:24 -0700)
committerGitHub <noreply@github.com>
Thu, 18 Oct 2018 05:24:02 +0000 (22:24 -0700)
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
test/regress/regress1/rr-verify/fp-arith.sy
test/regress/regress1/rr-verify/fp-bool.sy

index f310396d220e46cd68129c1c2320dfcb076b94ec..278c1033957d7cf404c8d6e7fe1a163e0886a319 100644 (file)
@@ -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.")
index cca2487d4ea2e9eaed82570cd7fff5126b854a9d..61dc19fbb75f5de9835e0d88f6efb17bb87383b5 100644 (file)
@@ -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.")
index 8792a594c10b22044b11d8b7474b371d1692dfa9..8e404668eba9bad741debe1dccf7598519cd3631 100644 (file)
@@ -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.")