projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 027ed26)
Fix regression output related to sygus+bv-div-zero (#4122)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 19 Mar 2020 22:57:42 +0000 (17:57 -0500)
committerGitHub <noreply@github.com>
Thu, 19 Mar 2020 22:57:42 +0000 (17:57 -0500)
test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 patch | blob | history

diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
index 72ece4064b61e8b09373286c88b9e5a0e61ce154..bc882fc8aa721a9211c99958d32bc9a774e140b1 100644 (file)
--- a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
+++ b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inference --fmf-bound --uf-ho --no-bv-div-zero-const
+; COMMAND-LINE: --sygus-inference --fmf-bound --uf-ho
 (set-logic ALL)
 (declare-fun a () (_ BitVec 1))
 (assert (bvsgt (bvsmod a a) #b0))