summaryrefslogtreecommitdiff
path: root/test/regress/regress1/ho/issue4065-no-rep.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/ho/issue4065-no-rep.smt2')
-rw-r--r--test/regress/regress1/ho/issue4065-no-rep.smt23
1 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2
index 9852150d9..a13aa2bae 100644
--- a/test/regress/regress1/ho/issue4065-no-rep.smt2
+++ b/test/regress/regress1/ho/issue4065-no-rep.smt2
@@ -1,7 +1,6 @@
-(set-logic AUFBV)
+(set-logic HO_AUFBV)
(set-info :status unsat)
(set-option :fmf-bound-int true)
-(set-option :uf-ho true)
(declare-fun _substvar_20_ () Bool)
(declare-sort S4 0)
(assert (forall ((q15 S4) (q16 (_ BitVec 20)) (q17 (_ BitVec 13))) (xor (= (_ bv0 13) (_ bv0 13) q17 (bvsrem (_ bv0 13) (_ bv0 13)) q17) _substvar_20_ true)))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback