From c77262836774c08d5c05fb057348b820a2643c07 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Dec 2017 22:26:17 -0600 Subject: Fixes for cbqi-bv (#1449) --- test/regress/regress0/quantifiers/Makefile.am | 3 ++- test/regress/regress0/quantifiers/model_6_1_bv.smt2 | 15 +++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/quantifiers/model_6_1_bv.smt2 (limited to 'test/regress/regress0/quantifiers') diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index bb43d6c1c..a8c25ae5a 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -134,7 +134,8 @@ TESTS = \ javafe.ast.WhileStmt.447.smt2 \ clock-10.smt2 \ javafe.tc.FlowInsensitiveChecks.682.smt2 \ - javafe.tc.CheckCompilationUnit.001.smt2 + javafe.tc.CheckCompilationUnit.001.smt2 \ + model_6_1_bv.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/model_6_1_bv.smt2 b/test/regress/regress0/quantifiers/model_6_1_bv.smt2 new file mode 100644 index 000000000..011430bd6 --- /dev/null +++ b/test/regress/regress0/quantifiers/model_6_1_bv.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --cbqi-nested-qe +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun lambda () (_ BitVec 32)) +(declare-fun lambdaprime () (_ BitVec 32)) +(declare-fun x5 () (_ BitVec 32)) +(declare-fun x4 () (_ BitVec 32)) +(declare-fun bool.b22 () Bool) +(declare-fun bool.b7 () Bool) +(declare-fun bool.b5 () Bool) +(declare-fun bool.b6 () Bool) +(assert (forall ((?lambda (_ BitVec 32))) (or (or (exists ((?lambdaprime (_ BitVec 32))) (let ((?v_1 (not bool.b22)) (?v_3 (not bool.b7)) (?v_4 (not bool.b5))) (let ((?v_2 (and ?v_4 (not bool.b6))) (?v_0 (bvmul (bvneg (_ bv1 32)) (bvadd x4 (bvmul (_ bv30 32) ?lambdaprime))))) (and (and (bvsle (_ bv0 32) ?lambdaprime) (bvsle ?lambdaprime ?lambda)) (not (and (not (bvsle (bvmul (bvneg (_ bv1 32)) (bvadd x5 (bvmul (_ bv1 32) ?lambdaprime))) (bvneg (_ bv10 32)))) (and (and (not (and (bvsle ?v_0 (bvneg (_ bv4100 32))) (and ?v_1 (and ?v_3 ?v_2)))) (not (and (bvsle ?v_0 (bvneg (_ bv4500 32))) (and ?v_1 (and bool.b7 ?v_2))))) (not (and (bvsle ?v_0 (bvneg (_ bv4910 32))) (and ?v_1 (and ?v_3 (and ?v_4 bool.b6)))))))))))) (bvslt ?lambda (_ bv0 32))) (not (and (not bool.b22) (and (not bool.b7) (and bool.b5 (not bool.b6)))))))) +(check-sat) +(exit) -- cgit v1.2.3