[Consolidated] Segfaults

[wintered]

81cb575

$z3release bug.smt2                                                             
[1]    3360378 segmentation fault  z3release bug.smt2                           
$cat bug.smt2                                                                   
(declare-fun a () String)                                                       
(set-option :proof true)                                                        
(assert (and (not (not (= 0 0))) (not (= 0 0))))                                
(check-sat-using qfufbv_ackr) 

[wintered]

81cb575

$z3release bug.smt2                                                             
[1]    802442 segmentation fault  z3release bug.smt2                            
$cat bug.smt2                                                                   
(declare-fun value2 () String)                                                  
(set-option :proof true)                                                        
(assert (and (= 0 0) (not (= 0 0))))                                            
(check-sat-using qffp) 

[wintered]

81cb575

$z3release horn.smt2                                                            
[1]    4083342 segmentation fault  z3release horn.smt2                          
$cat horn.smt2                                                                  
(assert (forall ((a Bool) (b Bool) (d (_ BitVec 1)) (e (_ BitVec 1)) (f (_ BitVec 1)) (g Bool))
(= (= f (ite a (_ bv0 1) (ite true (_ bv0 1) (ite b e e)))) g)))                
(check-sat-using horn) 

[wintered]

81cb575

$z3release bug.smt2                                                             
[1]    305949 segmentation fault  z3release bug.smt2                            
$cat bug.smt2                                                                   
(declare-fun a () Real)                                                         
(assert (and (> 0 0)))                                                          
(get-interpolant a true)

[NikolajBjorner]

I think the reality check here is "who cares" about these bugs?
You pass a non-Boolean argument to interpolation, which isn't even advertised functionality?
I fixed this one, but then who benefits vs. the overhead fixing?