diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-20 22:26:17 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-12-20 22:26:17 -0600 |
| commit | c77262836774c08d5c05fb057348b820a2643c07 (patch) | |
| tree | 42270c27fd63f355ab819ccaa3a9782f0115886b /test/regress | |
| parent | f9149d3b3e785950a846fb195bf9fa9cb1a2d94a (diff) | |
Fixes for cbqi-bv (#1449)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/model_6_1_bv.smt2 | 15 |
2 files changed, 17 insertions, 1 deletions
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) |