From 4190e79f22015de75a0c33ddda89d6b7ac2fd5c3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 19 Mar 2020 17:57:42 -0500 Subject: [PATCH] Fix regression output related to sygus+bv-div-zero (#4122) --- test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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)) -- 2.30.2