aqjune

open tactic

private constant mk_eq (sz:size) (x y:bitvector sz): x = y
constant smt_eq {sz:size}: sbitvec sz → sbitvec sz → Prop

theorem eq_add2 (sz:size): ∀ (x y: bitvector sz),
    smt_eq (sbitvec.add (sbitvec.of_bv x) (sbitvec.of_bv y))
           (sbitvec.of_bv (bitvector.add x y)) :=
by do
  x ← intro `x,

aqjune

/-
constant eq_test {sz:size}: sbitvec sz → bitvector sz → Prop
  

axiom eq_const (sz:size): ∀ (z:ℤ),
    eq_test (sbitvec.of_int sz z) (bitvector.of_int sz z)

meta instance eq_const_decidable (sz:size): decidable (∀ (z:ℤ),
    eq_test (sbitvec.of_int sz z) (bitvector.of_int sz z)) :=

aqjune

class C {α:ℕ → Type} :=
    (myf:α 1 → α 1 → α 1)
    (cx cy:α 1)

variable {α:ℕ → Type}
variable [s1:@C α]

include s1
def f1 := C.myf (C.cx α) (C.cy α)
def f2 := f1 /- don't know how to synthesize placeholder

aqjune

class C {α:ℕ → Type} :=
    (myf:α 1 → α 1 → α 1)
    (cx cy:α 1)

variable {α':ℕ → Type}
variable [s1:@C α']

include α'
include s1
def f1 := C.myf (C.cx α') (C.cy α')

aqjune

inductive any
| val : ∀ (α:Type), α → any

def bar (n:nat):option nat :=
  return n

def foo:option any :=
  do
  dummy ← bar 10,
  return (any.val nat 3)

aqjune

#include <vector>
#include <iostream>
#include<utility>
using namespace std;

class C {
public:
  int *ptr;
  C(int val) {
    cout << "  Constructor: " << (intptr_t) this << endl;

aqjune

define <4 x i8*> @tinkywinky() {
  %patatino = getelementptr i8, i8* undef, <4 x i64> undef
  ret <4 x i8*> %patatino
}
=>
define <4 x i8*> @tinkywinky() {
  ret <4 x i8*> undef
}

aqjune

unsigned fib(unsigned n) {
    unsigned answ;
    if (n <= 1)
        answ = n;
    else
        answ = fib(n - 1) + fib(n - 2);
    return answ;
}

aqjune

target datalayout="e"
;target datalayout="E" ; both is fine

define void @src(i8** %q) {
  %ofs = shl i64 7, 60
  %p = getelementptr i8, i8* null, i64 %ofs
  store i8* %p, i8** %q
  ret void
}

aqjune

diff --git a/llvm/lib/Transforms/InstCombine/InstCombineSelect.cpp b/llvm/lib/Transforms/InstCombine/InstCombineSelect.cpp
index 6a7fe9d707a2..ad4b13a52300 100644
--- a/llvm/lib/Transforms/InstCombine/InstCombineSelect.cpp
+++ b/llvm/lib/Transforms/InstCombine/InstCombineSelect.cpp
@@ -49,7 +49,7 @@ using namespace PatternMatch;
 
 /// FIXME: Enabled by default until the pattern is supported well.
 static cl::opt<bool> EnableUnsafeSelectTransform(
-    "instcombine-unsafe-select-transform", cl::init(true),
+    "instcombine-unsafe-select-transform", cl::init(false),