From d54c761087af01874ea6674111888cb94ffa4ee6 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Mon, 11 Jun 2012 18:54:38 +0000 Subject: fixing bitvector bugs * clauses shouldn't be erased when they could be a reason for outside propagation * propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally --- test/regress/regress0/bv/fuzz28.smt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress0/bv/fuzz28.smt') diff --git a/test/regress/regress0/bv/fuzz28.smt b/test/regress/regress0/bv/fuzz28.smt index 2c7a71a0f..732017750 100644 --- a/test/regress/regress0/bv/fuzz28.smt +++ b/test/regress/regress0/bv/fuzz28.smt @@ -1,6 +1,6 @@ (benchmark fuzzsmt :logic QF_BV -:status unknown +:status unsat :extrafuns ((v0 BitVec[4])) :extrafuns ((v1 BitVec[4])) :extrafuns ((v2 BitVec[4])) -- cgit v1.2.3