Skip to content

Commit

Permalink
cvc4: add test to expose current bug
Browse files Browse the repository at this point in the history
This breaks this formula, but the formula shouldn't currently be passing
its tests as it produces broken binaries on El Capitan.

Signed-off-by: Andrew Janke <andrew@apjanke.net>
  • Loading branch information
Adam C. Foltzer authored and apjanke committed May 6, 2016
1 parent fe5c0c5 commit 7727e75
Showing 1 changed file with 10 additions and 0 deletions.
10 changes: 10 additions & 0 deletions Formula/cvc4.rb
Expand Up @@ -45,5 +45,15 @@ def install
EOS
result = shell_output "#{bin}/cvc4 #{(testpath/"simple.cvc")}"
assert_match /valid/, result
(testpath/"simple.smt").write <<-EOS.undent
(set-option :produce-models true)
(set-logic QF_BV)
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
(assert (not s_1))
(check-sat)
EOS
result = shell_output "#{bin}/cvc4 --lang smt #{(testpath/"simple.smt")}"
assert_match /unsat/, result
end
end

0 comments on commit 7727e75

Please sign in to comment.