From: Andrew Reynolds Date: Thu, 19 Mar 2020 22:57:42 +0000 (-0500) Subject: Fix regression output related to sygus+bv-div-zero (#4122) X-Git-Tag: cvc5-1.0.0~3471 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4190e79f22015de75a0c33ddda89d6b7ac2fd5c3;p=cvc5.git Fix regression output related to sygus+bv-div-zero (#4122) --- diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 index 72ece4064..bc882fc8a 100644 --- 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))