S Spitans
email: spitans@etp.uni-hannover.de

E Baake

A Jakovics

Electromagnetic levitation melting of metals on a large scale: simulation and experiments

Keywords: levitation melting, scale-up, free surface flow, two-frequency field, numerical simulation, LES

In this paper, a drip-and leakage-free approach for electromagnetic (EM) levitation melting of metallic samples in horizontal and orthogonal two-frequency fields is studied further. The developed numerical model is used to investigate instabilities of liquid metal shape excited by the interaction of two-frequency EM fields and to design a scaled-up experimental setup for a stable levitation melting of 500 g of aluminum for further validation of the method.

Introduction

Induction melting of metals under complete levitation conditions has two main advantages over conventional ceramic crucible or cold crucible induction furnaces. EM levitation in a non-reactive atmosphere prevents contamination of the melt with the crucible material and results in a significantly enhanced purity of alloy. Moreover, heat losses from the liquid metal are limited only to radiation and evaporation that permits EM processing at extremely high temperatures.

The levitation melting was invented in the 1920's [START_REF] Muck | German Patent[END_REF], whereas the application started only thirty years later [START_REF] Okress | [END_REF] as the first high-frequency generators became available. The method is well known for measurements of thermophysical properties, such as viscosity, surface tension and heat conductivity of molten metals in experiments with small levitated droplets of 1-10 mm in diameter [3]. However, levitation melting obviously meets requirements for a growing number of large-scale industrial applications [4].

In axisymmetric EM levitation melting furnaces, the Lorentz force vanishes at the symmetry axis [5]. The melt outflow and leakage can be hindered at this lowest point on the axis of a levitated sample mainly by melt surface tension. Therefore, the charge weight is limited to 50-100 g [6], and industrial needs for the scale-up remain unsatisfied.

The new method applies two EM fields of different AC frequencies, whose field lines in the absence of a charge are horizontal and orthogonal in order to exert EM lift forces also at the axis of the levitated sample [7], [8]. Therefore, the charge weight can be increased and the charge can be drip-and leakage-free melted.

A numerical model for simulation and optimization of a particular EM levitation melting technology has been developed and verified previously [9]. Computation of EM induced flow and free surface dynamics is ensured by means of external coupling between EM force recalculation in ANSYS, Volume of Fluid (VOF) simulation of a two-phase turbulent flow in FLUENT, free surface shape reconstruction in CFD-Post and a self-written surface filtering procedure.

The method for EM levitation melting in horizontal fields has been successfully validated by a series of experiments and 3D calculations in a novel two-frequency EM levitation melting setup [10]. In this work the developed numerical model is used to investigate stability of contactless EM confinement in two-frequency horizontal and orthogonal fields and to design an experimental setup for a stable levitation melting of 500 g of aluminum.

Stability of a liquid metal column in a two-frequency EM field

In a simplified XY-planar consideration, the instant Lorentz force density component f x em in two-frequency (ω 1 and ω 2 ) EM fields can be written as follows:

where B Re , B Im , J Re and J Im are, respectively, the real and imaginary parts of the magnetic induction and current density complex amplitudes, the lower indices denote the spatial component and the EM field frequency. Inverting the x and y indices and neglecting the '-' sign in front of the force component will yield an expression for f y em . The terms in the first parentheses {} * are time-independent and correspond to the steady part of the Lorentz force. Note that eddy currents interact only with magnetic fields of the same frequency. That is why it is possible to apply the superposition principle to the Lorentz forces itself. In other words, the total steady Lorentz force induced by EM fields of two frequencies is the sum of the steady parts obtained separately in the first and in the second EM field.

The terms in the second parentheses {} ** stand for the oscillatory part of the Lorentz forces. It is a common practice to neglect them as they oscillate with a double EM field frequency. If the frequency is high enough, the melt is not able to react against the rapidly oscillating force due to inertia.

The terms in the third parentheses {} *** stand for the cross-interaction between eddy currents and magnetic fields of different frequencies. Terms, which oscillate with a frequency of ω 1 +ω 2 can be also neglected if the frequency is high, however, terms, which oscillate with a frequency of ω 1 -ω 2 can be neglected only if the difference of two frequencies is also high enough.

An appropriate choice of two different frequencies makes it possible to consider only the steady part of the Lorentz force and reduce computational efforts significantly. In order to prove that, we have developed a conceptual 2D-planar model of the two-frequency levitation melting setup from [10] (Fig. 1a) and considered oscillations of a liquid column in a two-frequency EM field.

At the initial time moment t = 0 s, the column has the initial radius r = 15 mm and zero velocity. The frequency f 1 is varied from 25000.25 Hz to 25020.00 Hz and the second frequency f 2 = 25000 Hz is fixed. Because f 1 and f 2 are in the range of several kHz, we neglect the Lorentz force terms with cos(2ω 1 t), cos(2ω 2 t) and cos((ω 1 +ω 2 )t). Only the steady part and the cos((ω 1 -ω 2 )t) term are considered. We ensure Lorentz force recalculation due to the changes of the shape, time evolution and track oscillations of the column radius r in the direction of the largest deformation (Fig. 1b).

In case of two different frequencies f 1 > f 2 , a typical period T = 1/(f 1 -f 2 ) can be calculated. At a time moment t = n•T (n = 0, 1, 2…), the melt is squeezed by the Lorentz forces in one direction and at t = n•T + T/2 in the orthogonal direction. At t = n•T + T/4 and t = n•T + 3T/4, the EM field, respectively, rotates clockwise and counter-clockwise and the melt is confined in both orthogonal directions. Because of only four poles, the azimuthal Lorentz force component is too small.

If the frequency difference is large enough, e.g., f 1 -f 2 = 20 Hz, the change of the Lorentz force is so fast that the melt is not able to respond. This results in negligible oscillations of a radius r and a steady flow pattern generated by the steady part of the Lorentz force (Fig. 1b). As the frequency difference f 1 -f 2 decreases, the amplitude r max -r min =Δr 0 of the fully developed oscillations increases (Fig. 1a). At f 1 -f 2 = 4 Hz, the oscillations of the liquid column evolve so fast that in less than 1 s the metal touches the ferrite pole, and it is not possible to detect Δr 0 (Fig. 1b). The resonance frequency appears to be the Rayleigh frequency f R for the fundamental oscillation mode [START_REF] Lamb | Hydrodynamics[END_REF]. In case of our 2D-planar column, it can be calculated as As we continue to decrease f 1 -f 2 , in the considered case of small inductor current, the oscillation amplitude Δr 0 goes down to a minimum (Fig. 1a). However, this part of the graph is dependent on the ratio between the electromagnetic and the surface tension forces and might have another maximum near f 1 =f 2 .

Eventually, in order to suppress the natural free surface oscillations and consider only the steady part of the Lorentz force, the frequency difference f 1 -f 2 must be much greater than the Rayleigh frequency f R . The requirement is easy to fulfill in practice, because the typical AC frequency range for the levitation melting is 1-100 kHz, whereas the fundamental mode is within several Hz.

Numerical simulation of EM levitation melting scale-up

Using the developed and verified numerical model, the two-frequency EM levitation melting furnace has been optimized to meet conditions for a stable levitation melting of 500 g of aluminum.

The final scale-up configuration has a ferrite yoke and two pairs of inductors arranged on the orthogonal lines (Fig. 2b). Each pair of the coils is fed by an effective current of I ef = 1.1 kA at frequencies f 1 = 30 kHz and f 2 = 40 kHz, accordingly. Both EM frequencies and their difference are high enough to consider only the steady part of the Lorentz force in our numerical simulation.

The specific shape of the yoke enhances the concentration of the magnetic field in the gap region. Alignment of the inner inductor turn at the inner edge of the ferrite poles reduces the parasitic magnetic field looping through the neighboring poles. The outer ferrite ring separates the closing magnetic flux that might decrease the magnetic field in the gap region.

A transient 3D simulation was performed, using a spherical free surface shape with a diameter of 7.5 cm and zero velocity at t = 0 s. As the flow became fully developed, the time averaging for the next 5 seconds was performed.

The close-up of the time averaged molten aluminum shape, the levitation melting furnace, as well as the symmetry planes of the inductor coils used for representation of the Lorentz force and melt velocity are shown in Fig. 2a. The lower part of the melt appears to be stable, as it is tightly confined by the high frequency EM field, whereas the upper part above the inductors is fluctuating due to the turbulent and unsteady flow. The Lorentz force minimum at the magnetic field separation points creates four bulges of the free surface next to the ferrite poles.

Experimental setup has been manufactured for validation of the simulated scaled-up configuration (Fig. 2c). Time-averaged results for the free surface shape, Lorentz force (Fig. 3a) and the flow (Fig. 3b), as well as the instant free surface shape and velocity (Fig. 3c), are shown on the orthogonal cross-sections. The Lorentz force domination at the bottom of the melt contributes to a formation of one torroidal vortex with a maximum velocity of 0.4 m/s.

The 3D transient calculation with a precise LES turbulence model shows that the levitation of 500 g of molten aluminum is possible in a horizontal two-frequency EM field configuration. Experimental validation of numerical results determines the future research.

Conclusions

••The appropriate choice of two different AC frequencies for levitation melting in horizontal fields makes it possible to account only for the steady part of the Lorentz force, therefore to avoid resonance with Rayleigh frequencies and to reduce computational efforts significantly.

••Using the developed and verified numerical approach, the design of the furnace has been tailored to meet the conditions of stable EM levitation of 500 g of molten aluminum.

••Experimental validation of numerical results for the scale-up configuration is on top of the day.

Fig. 1 :

 1 2D-planar model of the two-frequency levitation melting setup and simulation results for the liquid column oscillation amplitude Δr 0 dependence on f 1 -f 2 (a), as well as oscillation dynamics r(t) (b).

  Fig. 2: A 3D model of a scaled-up and optimized two-frequency EM levitation melting setup (b), a close-up of the time averaged shape of molten aluminum (m = 500 g) with two orthogonal planes for representation of results (b) and manufactured experimental setup for further validation of numerical model (c).

Fig. 3 :

 3 3D LES numerical results for the time-averaged free surface shape, Lorentz force (a) and velocity pattern (b), as well as instant flow (c) over the orthogonal cross-sections.

Acknowledgment

The current research was performed with the financial support of the ESF project of the University of Latvia, contract No. 2009/0138/1DP/1.1.2.1.2/09/IPIA/VIAA/004. The authors are grateful to the German Research Association for supporting this study under grant No. BA 3565/3-2. The authors would like to thank Prof. Dr.-Ing. O. Pesteanu (*1945- †2012) for the development of a particular technology and acknowledge his contribution and support in this research.


M Slazhniev

A Kizilova

K Bogdan

Developing of pragmatic models of the ponderomotive interactions in magnetodynamic installations for aluminum alloys MDN-6A

Keywords: magnetodynamic installation, ponderomotive interactions, electromagnetic force, model, efficiency

In this study the methods and device for "in real time mode" measurements of ponderomotive interactions, created in the working area of MDI by the volumetric electromagnetic forces is developed and tested. The pragmatic models of the ponderomotive interactions and electromagnetic force/pressure (f em /p em ) , in dependence from voltages (U ind , U em ) supplied on the coils of inducers and electromagnet has been studied and developed. Shown, that real efficiency T-shaped WA of MDI EM-pump makes 8÷12%, and inefficient losses and redistributions of the total volumetric electromagnetic force and created by it dynamic pressure makes up to 76%, that for seriously modernization of existing WA geometry is required. In addition, the value and dependence of the ponderomotive interactions, caused by the normal constituent of the AC (I) in the channel with magnetic field of inducer has been estimated and for dynamic control and improving of melt heating processes and stirring in induction furnaces and existing MDI can be applied.

Introduction

Improving of technological capabilities of the magnetodynamic installations for aluminium alloys (MDI) [START_REF] Polishchuk | Kyiv (Ukraine)[END_REF][START_REF] Lee | Proceedings of the 12th International Conference on Aluminium Alloys[END_REF] on today is focused on performance, it industrial application and satisfying to requirements in modern foundry both in Ukraine and abroad. Application of the existing MDI (on example MDN-6A) are known as mixer-batchers and die casting equipment.

In the induction channel furnace with electromagnetic pump, such as MHD-installation, the melt heating control, it electromagnetic transportation, mixing and processing there is provide by electromagnetic systems (inducers and an electromagnet) by changing the voltages, applied to it coils. Thus, in the classical application in MDN-6A for aluminum alloys, heating system is designed as a twin W-shaped induction channel with two inducers (Fig. 1), and creation of electromagnetic pressure performed in the area of it connection with central channel, that to forms the classic Tshaped (tee) working area (WA). WA by a both sides of the C-shaped electromagnet poles enclosed (Fig. 1) [START_REF] Polishchuk | Kyiv (Ukraine)[END_REF]. To monitor and control the intensity of heating of molten aluminum (TC/min) and creating of the electromagnetic pressure (Pem) previously has been used simple experimental empirical relations and indirect static models [START_REF] Lee | Proceedings of the 12th International Conference on Aluminium Alloys[END_REF][START_REF] Slazhniev | [END_REF]. Such models has been determined experimentally by measuring the rate of melt heating in the crucible (using inertial internal thermocouples) in depending from the suppling to inducers voltage (40 to 80 V), at inducing in the melt in induction channel the AC current from 5 to 15 kA. The electromagnetic pressure (Pem) in MDN-6A has been determined by measuring of the height of the metal level in metallduct (Fig. 1), at its rising above the surface in the crucible and further enumeration to the hydraulic pressure (P em = ρgh). At this for calculation the averaged density melt (ρ) in the molten state for set temperature (e.g. for aluminium alloy A356 at 700C density to be 2450 kg / m 3 ) has been used. But, such static (indirect) models doesn't provided the dynamical (in real time) monitoring and control of melt heating process and creating electromagnetic pressure (Pem), and did not providing the accuracy at discrete and continuous casting of aluminum into the crystallizer or casting mold, and has been a very high error (up to 20% or above). Additionally it cannot be use for automatic control (SAC) of the casting technologies [START_REF] Slazhniev | [END_REF][4][5], for example at controllable filling of chill-mold cavity at casting under low electromagnetic pressure and die-casting. Before by researchers of PTIMA NASU the row of theoretical mathematical models [START_REF] Polishchuk | Kyiv (Ukraine)[END_REF]6], based on Navier-Stokes equations, was developed. However, it practical application for operating of magnetodynamic pumps (such as MDN-6A) has been impossible, that the real component of p (pressure), u (flow velocity), ρ (density) and others too difficult for calculation at in-time mode and is need fitting the pragmatic model, based on measurements of performed on real industrial channel furnaces with electromagnetic pump. In order to this, from the technological view point, control and regulating of electromagnetic pressure at casting under low electromagnetic pressure to need, as primary, the direct measuring in-time electromagnetic force value in the WA of the magnetodynamic pump. Along with this, in work the develop of method and apparatus for direct real-time measurements of generated in the working area MDI electromagnetic force, by means measurement of ponderomotive interactions at using of the developed weighing equipment was set as primary a task. Such an approach the on-line measurement of the electromagnetic force would allow is perform the further control and regulation value of electromagnetic pressure in the EM-pump of MDI in dependence from voltages that are suppling the coils of electromagnet and inducer. Second task in measurements the real value of efficiency T-shaped WA for determining the efficient operation of EM pump in MDI and hydrodynamic redistribution of dynamic pressure was consist. Because the main problem of improving performance of the MDI to provide expense of created pressure (from 30 kPa to 50 kPa) are need. Third, in order to optimize and intensify heating the melt in induction channels of MDI (from 3 to 10 C/min) in accordance with the Navier-Stokes equations and Maxwell it was necessary in the first phase of work to develop the pragmatic models, based on the measurement of ponderomotive interactions in industrial MDN-6A at it working in the pump mode.

Developing methods and device for ponderomotive interactions measurements.

For providing of controlled electromagnetic pouring and discrete dosage the set portions (mass) of aluminium alloy (in a range 2÷400 kg with accuracy from 2.0% to 0.5%) in PTIMA NAS of Ukraine the magneto-weighting installation (MWI) [8] was designed. The MWI is a MDI (MDN-6A) which are combined with a weight measuring system (WMS), that allow to produce the continuous static and dynamic (in real time mode) high-precision measurement of the molten melt weight in crucible and channels with accuracy 0.1%. Especially for improving of the measurement accuracy, up to 0.2%, the MDI with integrated digital weight-measuring system (IWMS) [9] has been developed (Fig. 1). In this case, for measurement of melt weight in MDI-IWMS is used the four strain gauges sensors (BSA Shear beam load cell 500 kg, with accuracy 0.02%), mounted on chassis MDI and located under the crucible with W-shaped induction channel and aluminum molten melt inside. Each load cells was connected to a digital weight measuring indicator (microprocessor device CAS CI-8000V) for measuring and operating of dosage process at electromagnetic pouring of melt from MDI to casting mold via metalduct (for example). By such solution, the integrated digital weighting system (IWMS) measured only weight of crucible, metal-duct, W-shaped channel and lining inside and the variable mass of molten alloy (m crucible , m lining , m metduc , m melt ), and does not produce the weighting the inducers and electromagnet, that are divided from crucible and channel through air gap (Fig. 1). At the working MDI in the pumping mode on the aluminium alloy in crucible and W-shaped channel, there are acting a complex non-stationary magnetic fields and electromagnetic forces, named as a ponderomotive interactions [4,5,7]. Such ponderomotive interaction is directed vertically (unidirectionally with electromagnetic force Fem) and by means of the developed method and device it are measured, in weight equivalent (kg), by integrated weighting system as a "unload" impact (ΣF em.pond ). Additionally the ponderomotive interaction is proportional to the "rms value" of the pulsating electromagnetic forces Fem, which the hydraulic pressure (P) in molten aluminum alloy are create. ΣF em.pond -is a vector sum of vertically directed components of ponderomotive force, that is consist: F em.force -electromagnetic force, created in WA, N; F reac.constr -interaction of a magnetic field (B) with metallic case of W-shaped channel, near from poles of the C-shaped electromagnet, N; F rad.felectromagnetic interaction, caused by the tangential component of the AC (I) in aluminum alloy located in the channel with inducers magnetic fields, named as "radial force", N. In this case, the balance equation (1) do not include the constituent of the mass of the chassis and electromagnetic systems (m chassis + m em.systems = 0), but at the creation of electromagnetic force/pressure has of additional vertical "normal" constituent of ponderomotive interactions (F(m IWMS )×g -the value, measured by the IWMS, N):

Control panel

Control box

Power

[(m crucible + m metduct + m melt + m lining ) -(F emf + F reac.constr + F rad.f ) = F(m IWMS )] × g, Newton, (1)

Experimental researching of electromagnetic ponderomotive electromagnetic interactions

For developing of the pragmatic models of ponderomotive electromagnetic interaction in MDI is performed the experimental researches, at using of the magnetodynamic installation MDN-6A-0.25-M, that are equipped by IWMS (Fig. 1), with molten aluminum alloy (A356), mass from 100 to 250 kg, and at it temperature in range 680÷740C. For measure only of the ponderomotive electromagnetic interactions (in weight equivalent), before switching of MDI to "pump" mode, on the indicator of IWMS has been set zero value of "packaging", that determine as a static load ((m crucible + m met- duct + m melt + m lining ) × g = 0) [START_REF] Polishchuk | Kyiv (Ukraine)[END_REF]. In this case, on the indicator of IWMS the value (m IWMS ) was showing, that as a sum value of dynamic ponderomotive interaction in a weight equivalent, in "kg" by (1), and force balance was as (F emf + F reac.constr + F rad.f )/g = m IWMS was defined. At researching (ΣF em.pond ) as a primary argument (operating parameter) the voltage on inductors (U ind ) and electromagnet (U em ) was selected (ΣF em.pond = f(U ind , U em )). In addition, such model for developing of automatic control system (ACS) for next automation casting technologies can be use. Experimental dependences (ΣF em.pond = f(U ind , U em ) at switching MWI-IWMS in "pump" mode (inductors in common mode (AB-AB)) at stages of step-down transformer 1, 3 and 5 (42, 60 and 80 Volts on each) and at the variable voltages on the electromagnet coils, from 40 to 80 Volts (steps 1, 2, 3, 4, 5), had been researched. For each combination of U ind , U em the data from digital weight indicator (CI8000) are recording and fixing through an analog-digital converter (ADC) to a computer, for next recording it to dataset. In further the obtained dataset has been processed by means of mathematical programs (Mathcad, Matlab). The registered and statistically processed experimental data of ponderomotive interactions (ΣF em.pond ) had a ratio from -7.7 to -29 kg (75.5÷285 N), in range variation of U ind and U em from 40 to 80 Volts. The negative value of ΣF em.pond are explained that the electromagnetic force action at pumping aluminum alloy in WA MDI was directed vertically, that was impacted as a "unload" on IWMS (Fig. 1), [START_REF] Polishchuk | Kyiv (Ukraine)[END_REF]. At simplifying to two-factor dependence (ΣF em.pond = f(U ind , U em )), experimental data is most appropriate and was interpolated to 2nd degree quadratic polynomial pragmatic model ( 2) (correlation coefficient R = 99.5%). by velocity head [7], that at the creation of the maximum "passport" pressure in MDN-6A (p em = 30kPa) the maximal linear melt velocity (v melt ) in outside of WA are equaled to 4.9÷5.1 m/sec. This value in agreement to the maximal flow rate of Al-alloy from MDI (q = 13.5 kg/sec) at it pumping from WA via output cross-section (S out.tube =9.42×10 -4 m 2 ) to central channel (Fig. 2) and by Torricelli [START_REF] Slazhniev | [END_REF] (q = v melt S out.tube  Al ) has been set 5.1÷5.6 m/s. However, that p em =F em /S out.tube , that necessary for pressure 30÷35kPa the "effective" electromagnetic force (f* em ) makes 23.55÷31.84 N. This force is create the hydraulic pressure H (Fig. 1) in aluminum melt column in metallduct up to 1.25 m. However, the comparison of the effective electromagnetic force (f* em ) and measured by IWMS (ΣF em.pond ) the more than in 10 times differ (f* em ≈ (23.55÷31.84 N) << ΣF em.pond ≈ (260÷284.5 N) was shown, or in "ponderomotive weight equivalent" to relate as a 2.4÷3.25 kg up to 29.5 kg. This effect can be explained that the generated in WA volumetric electromagnetic force (F em.force ) is affected on upper projection (cross-section) T-WA. Because it total projection of EMF action is wider than output hole (S out.tube ) as shown on Fig. 2. Due to the non-optimal redistribution of F em.force and velocity head (v em ) in WA the double vortexes with vertical directions of rotating of melt in WA is appearing. It the main hydraulic losses and reasons of instability working of WA (for example -appearing of EM pressure oscillation from 0.4 to 4Hz [START_REF] Slazhniev | [END_REF]) is formed, and the real efficiency of Tshaped WA (efficient operation of EM-pump of MDI) in the hydraulic system "WA-central branch W-shaped channelmetallduct" have ≈ 8.2 ÷ 11.2% ( hydr ≈ 0.08 ÷ 0.12).

To convert the measured by IWMS ponderomotive interactions (ΣF em.pond (U ind , U em ) to the effective (useful) electromagnetic force (f* em = k loss ×∑F em.int ) and hydraulic pressure (h em ) to equation ( 2) has been calculated and in it has been inputted the correlation coefficients (k loss ), which characterizing the "total" losses in the T-shape WA -[h(ΣF em.pond ) = k loss × (ΣF em.pond / S out.tube )/( Al × g), meter] (Fig. 3). Wherein, k loss ≈ 0.083÷0.112 at 660÷760C of aluminium alloys. By developed method the other components of the ponderomotive interactions in MDI, such as radial forces (F rad.f ), interactions with the construction (F reac.constr ) has been researched and processed up to pragmatic models [START_REF] Slazhniev | [END_REF]4).

F rad.f (U ind ) = -( 0.021739 × U ind + 0.1391)×g, N (3)
F reac.constr (U em ) = -(6.1×10 -4 U em 2 -0.373×U em + 1.1687)×g, N

Range of F reac.constr (U em ) (4), in depending from the voltages on electromagnet windings, has makes from -7 to -18 N (-0.7 to -1.8 kg) and makes of the 6 ÷ 7% of external magnetic flux irretrievable losses inside the metallic construction and parts of MDI (Fig. 3). The magnitude of "engine effect", named in study as a F rad.f (U ind ) (3), in the weight equivalent of ponderomotive interaction makes from -1.1 to -1.8 kg (-10.7 ÷ -17.7 N) (Fig. 3). During researching F rad.f (U ind ) there are indicated a vertical ponderomotive interactions, that is equaled to the equidistant (in experiment 50 mm) of inducers in relation to liquid-metal coil with electric current (AC) and it density (j). Scientific and practical interest of radial ponderomotive interactions can be used for continuous dynamic monitoring and control of the melt heating process and it stirring into channel-induction furnaces and in it crucibles. By performed study, the obtained pragmatic models (2-4) can be used for next further optimization of MDI modes of using, for developing the ACS for different casting technologies with MDI applying, and for further developing of the numerical model of fluid flow located in non-stationary magnetic field, fully coupling between Navier-Stokes and Maxwell equations can be applied also.

Conclusion

By measurements of ponderomotive interactions at using of the weighing equipment, the original method and apparatus for direct real-time measurements of generated in the working area MDI electromagnetic force first was developed and tested. For just developed device the balance force equation, including the detail analysis by ponderomotive force interactions in magnetodynamic installation (MDN-6A) was performed. The pragmatic models of the ponderomotive interactions and electromagnetic force/pressure (f em /p em ), in dependence from voltages (U ind , U em ), supplied on the coils of inducers and electromagnet studied and developed. The study of the redistribution of the electromagnetic forces in MDI for creation useful pressure are shown that real efficiency T-shaped WA of MDI EM-pump makes 8÷12 %. The inefficient losses of the total volumetric electromagnetic force makes up to 76% that the geometry of existing WA in MDI is required. From the practical interest of obtained pragmatic models application, it is can be used for further developing of the numerical model of fluid flow located in non-stationary magnetic field for aluminum induction channel furnaces with EM-pump, and for optimization of casting technologies with using of magnetodynamic installations for aluminum alloys.

Fig. 1 :

 1 Fig. 1: Structural and functional diagram of MDI with integrated weight-measuring system (MDI-IWMS).

Fig. 2 :Fig. 3 :

 23 Fig. 2: Scheme EM-interactions redistribution and hydraulic features in T-shaped WA MDI


Andrew Reynolds

Jasmin Christian Blanchette

Simon Cruanes

Cesare Tinelli

Model Finding for Recursive Functions in SMT

come   L'archive ouverte pluridisciplinaire

Introduction

Many solvers based on SMT (satisfiability modulo theories) can reason about quantified formulas using incomplete instantiation-based methods [START_REF] De Moura | Efficient E-matching for SMT solvers[END_REF][START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF]. These methods work well for proving the unsatisfiability of an input set of formulas, but they are of little help for finding models of them when they are satisfiable. Often, a single universal quantifier in one of the axioms of a problem is enough to prevent the discovery of models.

In the past few years, techniques have been developed to find models for quantified formulas in SMT. Ge and de Moura [START_REF] Ge | Complete instantiation for quantified formulas in satisfiability modulo theories[END_REF] introduced a complete instantiation-based procedure for formulas in the essentially uninterpreted fragment. This fragment is limited to universally quantified formulas where all variables occur as direct subterms of uninterpreted functions, as in ∀x : Int. f(x) ≈ g(x) + 5. Other syntactic criteria extend this fragment slightly, including cases when variables occur as arguments of arithmetic predicate symbols. Subsequently, Reynolds et al. [START_REF] Reynolds | Finite model finding in SMT[END_REF][START_REF] Reynolds | Quantifier instantiation techniques for finite model finding in SMT[END_REF] introduced techniques for finding finite models for quantified formulas over uninterpreted types and types having a fixed finite interpretation. These techniques can find a model for a formula such as ∀x, y : τ. x ≈ y ∨ ¬ f(x) ≈ f(y), where τ is an uninterpreted type.

Unfortunately, none of these fragments can accommodate the vast majority of quantified formulas that correspond to recursive function definitions. The essentially uninterpreted fragment does not allow the argument of a recursive function to be used inside a complex term on the right-hand side of the definition, whereas the finite model finding techniques are not applicable for functions over infinite domains such as the integers or algebraic datatypes. A simple example where both approaches fail is

∀x : Int. p(x) ≈ ite x ≤ 0, 1, 2 * p(x -1)
where ite is the 'if-then-else' operator. This state of affairs is unsatisfactory, given the frequency of recursive definitions in practice.

We present a method for translating formulas involving recursive function definitions into formulas where finite model finding techniques can be applied. The definitions must meet a semantic criterion to be admissible (Section 2). This criterion is general enough to include well-founded (terminating) recursive function definitions and restrictive enough to exclude inconsistent equations such as ∀x : Int. f(x) ≈ f(x) + 1.

We define a translation for a class of formulas involving admissible recursive function definitions (Section 3). A recursive equation ∀x : τ. f(x) ≈ t is translated to ∀a : α τ . f(γ f (a)) ≈ t[γ f (a)/x], where α τ is an "abstract" uninterpreted type and γ f : α τ → τ is an uninterpreted function from α τ to the corresponding concrete type τ. Additional constraints ensure that the abstract values that are relevant to the formula's satisfiability exist. The translation preserves satisfiability and, for admissible definitions, unsatisfiability, and makes finite model finding possible for problems in this class.

The approach is implemented as a preprocessor in the SMT solver CVC4 and in a new higher-order model finder called Nunchaku (Section 4). We evaluated the two implementations on benchmarks from IsaPlanner [START_REF] Johansson | Case-analysis for rippling and inductive proof[END_REF], Leon [START_REF] Blanc | An overview of the Leon verification system-Verification by translation to recursive functions[END_REF], and Isabelle/HOL, to demonstrate that this translation improves the effectiveness of the SMT solvers CVC4 and Z3 in finding countermodels to verification conditions (Section 5). Unlike earlier work, our approach relies on off-the-shelf SMT solvers (Section 6).

An earlier version of this paper was presented at the SMT 2015 workshop in San Francisco [START_REF] Reynolds | Model finding for recursive functions in SMT[END_REF]. This paper extends the workshop paper with proof sketches, an expanded implementation section covering Nunchaku and relevant CVC4 optimizations, and the evaluation on Isabelle benchmarks produced by Nunchaku.

Preliminaries

Our setting is a monomorphic (or many-sorted) first-order logic like the one defined by SMT-LIB [START_REF] Barrett | The SMT-LIB standard-Version 2.5[END_REF]. A signature Σ consists of a set Σ ty of first-order types (or sorts) and a set Σ f of function symbols over these types. We assume that signatures always contain a Boolean type Bool and constants , ⊥ : Bool for truth and falsity, an infix equality predicate ≈ : τ × τ → Bool for each τ ∈ Σ ty , standard Boolean connectives (¬ , ∧, ∨, etc.), and an if-then-else function symbol ite : Bool × τ × τ → τ for each τ ∈ Σ ty . We fix an infinite set Σ v τ of variables of type τ for each τ ∈ Σ ty and define Σ v as τ∈Σ ty Σ v τ . (Well-typed) Σ-terms are built as usual over functions symbols in Σ and variables in Σ v . Formulas are terms of type Bool. We write t τ to denote terms of type τ and T (t) to denote the set of subterms in t. Given a term u, a variable tuple x = (x τ 1 1 , . . . , x τ n n ) and a term tuple t = (t τ 1 1 , . . . , t τ n n ), we write u[t/x] to denote the result of simultaneously replacing all occurrences of x i with t i in u, for each i = 1, . . . , n.

A Σ-interpretation I maps each type τ ∈ Σ ty to a nonempty set τ I , the domain of τ in I, each function symbol f :

τ 1 × • • • × τ n → τ in Σ f to a total function f I : τ I 1 × • • • × τ I n → τ I , and each variable x : τ of Σ v to an element of τ I . A theory is a pair T = (Σ, I )
where Σ is a signature and I is a class of Σ-interpretations, the models of T , closed under variable reassignment (i.e., for every I ∈ I , every Σ-interpretation that differs from I only on the variables of Σ v is also in I ). A Σ-formula ϕ is T -satisfiable if it is satisfied by some interpretation in I . A formula ϕ T -entails ψ, written ϕ T ψ, if all interpretations in I that satisfy ϕ also satisfy ψ. Two formulas ϕ and ψ are T -

equivalent if each T -entails the other. If T 1 = (Σ 1 , I 1 ) is a theory and Σ 2 is a signature with Σ f 1 ∩ Σ f 2 = / 0, the extension of T 1 to Σ 2 is the theory T = (Σ, I ) where Σ f = Σ f 1 ∪ Σ f 2 , Σ ty = Σ ty 1 ∪ Σ ty 2
, and I is the set of all Σ-interpretations I whose Σ 1 -reduct is a model of T 1 . We refer to the symbols of Σ 2 that are not in Σ 1 as uninterpreted. For the rest of the paper, we fix a theory T = (Σ, I ) with uninterpreted symbols constructed as above.

Unconventionally, we consider annotated quantified formulas of the form ∀ f x. ϕ, where f ∈ Σ f is uninterpreted. Their semantics is as for standard quantified formulas ∀x. ϕ. Given f :

τ 1 × • • • × τ n → τ, a formula ∀ f x. ϕ is a function definition ( for f ) if
x is a tuple of variables x τ 1 1 , . . . , x τ n n and ϕ is a quantifier-free formula T -equivalent to f(x) ≈ t for some term t of type τ. We write ∃x. ϕ as an abbreviation for ¬ ∀x. ¬ ϕ.

Definition 1. A formula ϕ is in definitional form with respect to {f 1 , . . . , f n } ⊆ Σ f if it is of the form (∀ f 1 x 1 . ϕ 1 ) ∧ • • • ∧ (∀ f n x n . ϕ n ) ∧ ψ, where f 1 , . . . , f n are distinct function symbols, ∀ f i x i . ϕ i
is a function definition for i = 1, . . . , n, and ψ contains no function definitions. We call ψ the goal of ϕ.

In the signature Σ, we distinguish a subset Σ dfn ⊆ Σ f of defined uninterpreted function symbols. We consider Σ-formulas that are in definitional form with respect to Σ dfn .

Definition 2. Given a set of function definitions

∆ = {∀ f 1 x 1 . ϕ 1 , . . . , ∀ f n x n . ϕ n }, a ground formula ψ is closed under function expansion with respect to ∆ if ψ T n i=1 {ϕ i [t/x i ] | f i (t) ∈ T (ψ)}
The set ∆ is admissible if for every T -satisfiable formula ψ closed under function expansion with respect to ∆, the formula ψ ∧ ∆ is also T -satisfiable.

Admissibility is a semantic criterion that must be satisfied for each function definition before applying our translation, described in Section 3. It is useful to connect it to the standard notion of well-founded function definitions, often called terminating definitions. In such definitions, all recursive calls are decreasing with respect to a wellfounded relation, which must be supplied by the user or inferred automatically using a termination prover. This ensures that the function is uniquely defined at all points.

First-order logic has no built-in notion of computation or termination. To ensure that a function specification is well founded, it is sufficient to require that the defined function be terminating when seen as a functional program, under some evaluation order. For example, the definition ∀x : Int. p(x) ≈ ite x ≤ 0, 1, 2 * p(x -1) , where the theory T is integer arithmetic extended with p : Int → Int, can be shown to be well founded under a strategy that evaluates the condition of an ite before evaluating the relevant branch, ignoring the other branch. Logically, such dependencies can be captured by congruence rules. Krauss developed these ideas in the general context of higher-order logic [24, Section 2], where theories such as integer arithmetic can be axiomatized. Theorem 3. If ∆ is a set of well-founded function definitions for Σ dfn = {f 1 , . . . , f n }, then it is admissible. Proof sketch. Let ψ be a satisfiable formula closed under function expansion with respect to ∆. We show that ψ ∧ ∆ is also satisfiable. Let I be a model of ψ, and let I 0 be the reduct of I to the function symbols in Σ f \ Σ dfn . Because well-founded definitions uniquely characterize the interpretation of the functions they define, there exists a Σ-interpretation I that extends I 0 such that I ∆. Since ψ is closed under function expansion, it already constrains the functions in Σ dfn recursively as far as is necessary for interpreting ψ. Thus, any point v for which f I i (v) is needed for interpreting ψ will have its expected value according to its definition and hence coincide with I . And since ψ I does not depend on the interpretation at the other points, I is, like I, a model of ψ. Since I ∆ by assumption, we have I ψ ∧ ∆ as desired.

Another useful class of function definitions is that of productive corecursive functions. Corecursive functions are functions to a coalgebraic datatype. These functions can be ill founded without their being inconsistent. Intuitively, productive corecursive functions are functions that progressively reveal parts of their potentially infinite output [START_REF] Atkey | Productive coprogramming with guarded recursion[END_REF][START_REF] Turner | Elementary strong functional programming[END_REF]. Given a type of infinite streams of integers constructed by scons : int×stream → stream, the function defined by ∀ e x. e(x) ≈ scons(x, e(x + 1)) falls within this class: Each call to e produces one constructor before entering the next call. Like terminating recursion, productive corecursion totally specifies the functions it defines, and the proof of Theorem 3 can be adapted to cover that case: Theorem 4. If ∆ is a set of productive function definitions for Σ dfn , then it is admissible.

It is even possible to mix recursion and corecursion in the same function [START_REF] Blanchette | Foundational extensible corecursion: A proof assistant perspective[END_REF] while preserving totality and admissibility. Beyond totality, an admissible set can contain underspecified functions such as ∀ f x : Int. f(x) ≈ f(x) or ∀ g x. g(x) ≈ g(x + 1). The latter is problematic operationally, because in general the closure of a formula ψ that depends on some term f(a) is an infinite set {ψ} ∪ {g(a + k) ≈ g(a + k + 1) | k ≥ 0}. A similar issue arise with corecursive definitions specifying infinite acyclic objects, such as the e stream introduced above. Nonetheless, admissibility is still useful if the problem does not refer to g or e, because it tells us that we can safely ignore their definitions. We conjecture that it is safe to ignore all tail-recursive calls (i.e., calls that occupy the right-hand side of the definition, potentially under some ite branch) when establishing well-foundedness or productivity, without affecting admissibility.

An example of an inadmissible set is {∀ f x : Int. f(x) ≈ f(x) + 1}, where T is integer arithmetic extended to a set of uninterpreted symbols {f, g : Int → Int, . . .}. The set is inadmissible because the formula is closed under function expansion with respect to this set (since f does not occur in ), and yet there is no model of T satisfying f's definition. A more subtle example is

{∀ f x : Int. f(x) ≈ f(x), ∀ g x : Int. g(x) ≈ g(x) + f(x)}.
While this set has a model where f and g are interpreted as the constant function 0, it is not admissible since f(0) ≈ 1 is closed under function expansion and yet there exists no interpretation satisfying both f(0) ≈ 1 and g's definition.

The Translation

For the rest of the section, let ϕ be a Σ-formula in definitional form with respect to Σ dfn whose definitions are admissible. We present a method that constructs an extended signature E(Σ) and an E(Σ)-formula ϕ such that ϕ is T -satisfiable if and only if the

A 0 (t τ , p) = if τ = Bool and t = b(t 1 , . . . , t n ) then let (t i , χ i ) = A 0 (t i , pol(b, i, p)) for i = 1, . . . , n in let χ = χ 1 ∧ • • • ∧ χ n in if p = pos then b(t 1 , . . . , t n )) ∧ χ, else if p = neg then b(t 1 , . . . , t n ) ∨ ¬ χ, else b(t 1 , . . . , t n ), χ else if t = ∀ f x. u then let (u , χ) = A 0 (u, p) in ∀a : α f . u [γ f (a)/x], else if t = ∀x. u then let (u , χ) = A 0 (u, p) in ∀x. u , ∀x. χ else t, {∃a : α f . γ f (a) ≈ s | f(s) ∈ T (t), f ∈ Σ dfn } A(ϕ) = let (ϕ , χ) = A 0 (ϕ, pos) in ϕ Fig. 1. Definition of translation A Σ-formula ϕ is T -satisfiable-i.e.
, ϕ and ϕ are equisatisfiable (in T ). The idea behind this translation is to use an uninterpreted type α f to abstract the set of relevant input tuples for each defined function f and restrict the quantification of f's definition to a single variable of this type. Informally, the relevant input tuples t of a function f are the ones for which the interpretation of f(t) is relevant to the satisfiability of ϕ. More precisely, for each f :

τ 1 × • • • × τ n → τ ∈ Σ dfn , the extended signature E(Σ) contains an uninterpreted abstract type α f abstracting the Cartesian product τ 1 × • • • × τ n and n uninterpreted concretization functions γ f,1 : α f → τ 1 , . . . , γ f,n : α f → τ n .
The translation A defined in Figure 1 translates the Σ-formula ϕ into the E(Σ)formula ϕ . It relies on the auxiliary function A 0 , which takes two arguments: the term t to translate and a polarity p for t, which is either pos, neg, or none. A 0 returns a pair (t , χ), where t is a term of the same type as t and χ is an E(Σ)-formula.

The translation alters the formula ϕ in two ways. First, it restricts the quantification on function definitions for f to the corresponding uninterpreted type α f , inserting applications of the concretization functions γ f,i as needed. Second, it augments ϕ with additional constraints of the form ∃a : α f . γ f (a) ≈ s, where γ f (a) ≈ s abbreviates the formula n i=1 γ f,i (a) ≈ s i with s = (s 1 , . . . , s n ). These existential constraints ensure that the restricted definition for f covers all relevant tuples of terms, namely those occurring in applications of f that are relevant to the satisfiability of ϕ. The constraints are generated as deep in the formula as possible, based on the polarities of Boolean connectives, to allow models where the sets denoted by the α f types are as small as possible.

If t is an application of a predicate symbol b, including the operators ¬, ∧, ∨, ≈, and ite, A 0 calls itself recursively on the arguments t i and polarity pol(b, i, p), with pol defined as

pol(b, i, p) =    p if either b ∈ {∧, ∨} or b = ite and i ∈ {2, 3} -p if b = ¬ none otherwise
where -p is neg if p is pos, pos if p is neg, and none if p is none. The term t is then reconstructed as b(t 1 , . . . , t n ) where each t i is the result of the recursive call with argument t i . If the polarity p of t is pos, A 0 conjunctively adds to b(t 1 , . . . , t n ) the constraint χ derived from the subterms and returns as the constraint. Dually, if p is neg, it adds a disjunction with the negated constraint to produce the same net effect (since

¬ (φ ∨ ¬ χ) ⇐ ⇒ ¬ φ ∧ χ). It p is none, the constraint χ is returned to the caller.
If t is a function definition, A 0 constructs a quantified formula over a single variable a of type α f and replaces all occurrences of x in the body of that formula with γ f (a). (Since function definitions are top-level conjuncts, χ must be and can be ignored.)

If t is an unannotated quantified formula, A 0 calls itself on the body with the same polarity; a quantifier is prefixed to the quantified formula and constraint returned by the recursive call. Otherwise, t is either an application of an uninterpreted predicate symbol or a term of a type other than Bool. Then, the returned constraint is a conjunction of formulas of the form ∃a : α f . γ f (a) ≈ s for each subterm f(s) of t such that f ∈ Σ dfn . Such constraints, when asserted positively, ensure that some element in the abstract domain α f is the preimage of the argument tuple s.

Example 5. Let T be linear integer arithmetic with the uninterpreted symbols {c : Int, s : Int → Int}. Let ϕ be the Σ-formula

∀ s x : Int. ite x ≤ 0, s(x) ≈ 0, s(x) ≈ x + s(x -1) ∧ s(c) > 100 (1)
The definition of s specifies that it returns the sum of all positive integers up to x. The formula ϕ is in definitional form with respect to Σ dfn and states that the sum of all positive numbers up to some constant c is greater than 100. It is satisfiable with a model that interprets c as 14 or more. Due to the universal quantifier, SMT solvers cannot find a model for ϕ. The signature E(Σ) extends Σ with the type α s and the function symbol γ s : α s → Int. The result of A(ϕ), after simplification, is the E(Σ)-formula

∀a : α s . ite γ s (a) ≤ 0, s(γ s (a)) ≈ 0, s(γ s (a)) ≈ γ s (a) + s(γ s (a) -1) ∧ ∃b : α s . γ s (b) ≈ γ s (a) -1 ∧ s(c) > 100 ∧ ∃a : α s . γ s (a) ≈ c (2)
The universal quantifier in formula (2) ranges over an uninterpreted type α s , making it amenable to the finite model finding techniques by Reynolds et al. [START_REF] Reynolds | Finite model finding in SMT[END_REF][START_REF] Reynolds | Quantifier instantiation techniques for finite model finding in SMT[END_REF], implemented in CVC4, which search for a finite interpretation for α s . Furthermore, since all occurrences of the quantified variable a are beneath applications of the uninterpreted function γ s , the formula is in the essentially uninterpreted fragment, for which Ge and de Moura [START_REF] Ge | Complete instantiation for quantified formulas in satisfiability modulo theories[END_REF] provide a complete instantiation procedure, implemented in Z3. As expected, CVC4 and Z3 run indefinitely on formula (1). However, they produce a model for (2) within 100 milliseconds.

Note that the translation A results in formulas whose models (i.e., satisfying interpretations) are generally different from those of ϕ. One model I for formula (2) in the above example interprets α s as a finite set {u 0 , . . . , u 14 }, γ s as a finite map u i → i for i = 0, . . . , 14, c as 14, and s as the almost constant function λx : Int. ite(x ≈ 0, 0, ite(x ≈ 1, 1, ite(x ≈ 2, 3, ite(. . . , ite(x ≈ 13, 91, 105). . .))))

In other words, s is interpreted as a function mapping x to the sum of all positive integers up to x when 0 ≤ x ≤ 13, and 105 otherwise. The Σ-reduct of I is not a model of the original formula (1), since I interprets s(n) as 105 when n < 0 or n > 14.

However, under the assumption that the function definitions in Σ dfn are admissible, A(ϕ) is equisatisfiable with ϕ for any ϕ. Moreover, the models of A(ϕ) contain pertinent information about the models of ϕ. For example, the model I for formula [START_REF] Barrett | CVC4[END_REF] given above interprets c as 14 and s(n) as ∑ n i=1 i for 0 ≤ n ≤ 14, and there exists a model of formula (1) that also interprets c and s(n) in the same way (for 0 ≤ n ≤ 14). In general, for every model of A(ϕ), there exists a model of ϕ that coincides with it on its interpretation of all function symbols in Σ f \ Σ dfn . Furthermore, the model of A(ϕ) will also give correct information for the defined functions at all points belonging to the domains of the corresponding abstract types α f . This can sometimes help users debug their function definitions.

We sketch the correctness of translation A. For a set of ground literals L, we write X(L) to denote the set of constraints that force the concretization functions to have the necessary elements in their range for determining the satisfiability of L with respect to the function definitions in the translation. Formally,

X(L) = {∃a : α f . γ f (a) ≈ t | f(t) ∈ T (L), f ∈ Σ dfn } (3)
The following lemma states the central invariant behind the translation A. Proof sketch. First, we show that if ϕ is satisfied by an Σ-interpretation I, then A(ϕ) is satisfied by an E(Σ)-interpretation I . Let I be the E(Σ)-interpretation that interprets all types τ ∈ Σ ty as τ I , all functions f ∈ Σ f as f I , and for each function f :

τ 1 ו • •×τ n → τ in Σ dfn , interprets α f as τ I 1 × • • • × τ I
n and each γ f,i as the ith projection on such tuples for i = 1, . . . , n. Since I satisfies ϕ, it satisfies a set of ground literals L that entail ϕ. Furthermore, I satisfies every constraint of the form ∃a : α f . γ f (a) ≈ t, since by our construction of I there exists a value v ∈ α f I such that v = t I . Thus, I satisfies L ∪ X(L), and by Lemma 7 we conclude I satisfies A(ϕ).

Second, we show that if A(ϕ) is satisfied by a E(Σ)-interpretation I , then ϕ is satisfied by a Σ-interpretation I. Since ϕ is in definitional form with respect to the functions defined by ∆, it must be of the form ∆ ∧ ϕ 0 . First, we define a sequence of Σ-literals sets

L 0 ⊆ L 1 ⊆ • • • such that I satisfies L i ∪ X(L i ) for i = 0, 1, . . .

. Since

I satisfies A(ϕ 0 ), by Lemma 7, I satisfies a set of literals L ∪ X(L) where L is a set of Σ-literals that entail ϕ 0 . Let L 0 = L. For each i ≥ 0, let ψ i be the formula

{A(ϕ f [t/x]) | f(t) ∈ T (L i ), f ∈ Σ dfn }, where ∀ f x. ϕ f ∈ ∆. Since I satisfies A(∀ f x. ϕ f )
and X(L i ), we know that I also satisfies ψ i . Thus by Lemma 7, I satisfies a set of literals L ∪ X(L) where L is a set of Σ-literals that entail ψ i . Let L i+1 = L 0 ∪ L. Let L ∞ be the limit of this sequence (i.e., ∈ L ∞ if and only if ∈ L i for some i), and let ψ be the Σ-formula L ∞ . To show that ψ is closed under function expansion with respect to ∆, we first note that by construction ψ entails ψ ∞ . For any function symbol f and terms t, since ϕ f [t/x] does not contain function definitions, by Lemma 7,

A(ϕ f [t/x]) entails ϕ f [t/x]. Thus, ψ entails {ϕ f [t/x] | f(t) ∈ T (ψ), f ∈ Σ dfn }, meaning that
ψ is closed under function expansion with respect to ∆. Furthermore, ψ entails ϕ 0 since L 0 ⊆ L ∞ . Since ψ is a T -satisfiable formula that is closed under function expansion and ∆ is admissible, by definition there exists a Σ-interpretation I satisfying ψ ∧ ∆, which entails ∆ ∧ ϕ 0 , i.e., ϕ.

The intuition of the above proof is as follows. First, A(ϕ) cannot be unsatisfiable when ϕ is satisfiable since any Σ-interpretation that satisfies ϕ can be extended in a straightforward way to an E(Σ)-interpretation that satisfies A(ϕ), by interpreting the abstract types in the same way as the Cartesian products they abstract, thereby satisfying all existential constraints introduced by A. Conversely, if a model is found for A(ϕ), existential constraints introduced by A ensure that this model also satisfies a Σ-formula that is closed under function expansion and that entails the goal of ϕ. This implies the existence of a model for ϕ provided that ∆ is admissible.

We give an intuition of Theorem 8 in the context of an example.

Example 9. Let us revisit the formulas in Example 5. If the original formula ( 1) is T -satisfiable, the translated formula ( 2) is clearly also T -satisfiable since α s can be interpreted as the integers and γ s as the identity function. Conversely, we claim that (2) is T -satisfiable only if (1) is T -satisfiable, noting that the set {∀ s x. ϕ s } is admissible, where ϕ s is the formula ite x ≤ 0, s(x) ≈ 0, s(x) ≈ x + s(x -1) . Clearly, any interpretation I satisfying formula (2) satisfies L 0 ∪ X(L 0 ), where L 0 = {s(c) > 100} and X(L 0 ), defined by equation (3), consists of the single constraint ∃a : α s . γ s (a) ≈ c. Since I also satisfies both the translated function definition for s (the first conjunct of (2)) and X(L 0 ), it must also satisfy

ite c ≤ 0, s(c) ≈ 0, s(c) ≈ c + s(c -1) ∧ ∃b : α s . γ s (b) ≈ c -1
The existential constraint in the above formula ensures that whenever I satisfies the set L 1 = L 0 ∪ {¬ c ≤ 0, s(c) ≈ c + s(c -1)}, I satisfies X(L 1 ) as well. Hence, by repeated application of this reasoning, it follows that a model of formula (2) that interprets c as n must also satisfy ψ:

s(c) > 100 ∧ n-1 i=0 ¬ (c -i ≤ 0) ∧ s(c -i) ≈ c -i + s(c -i -1) ∧ c -n ≤ 0 ∧ s(c -n) ≈ 0
This formula is closed under function expansion since it entails ϕ s [(ci)/x] for i = 0, . . . , n and contains only s applications corresponding to s(ci) for i = 0, . . . , n. Since {∀ s x. ϕ s } is admissible, there exists a Σ-interpretation satisfying ψ ∧ ∀ s x. ϕ s , which entails formula (1).

Implementations

We have implemented the translation A in two separate systems, as a preprocessor in CVC4 (version 1.5 prerelease) and in the CVC4-based higher-order model finder Nunchaku. This section describes how the translation is implemented in each system, as well as optimizations used by CVC4 to find models of translated problems.

CVC4

In CVC4, function definitions ∀ f x. ϕ can be written using the define-fun-rec command from SMT-LIB 2.5 [START_REF] Barrett | The SMT-LIB standard-Version 2.5[END_REF]. Formula (1) from Example 5 can be specified as (define-fun-rec s ((x Int)) Int (ite (<= x 0) 0 (+ x (s (-x 1))))) (declare-fun c () Int) (assert (> (s c) 100)) (check-sat)

When reading this input, CVC4 adds the annotated quantified formula

∀ s x. s(x) ≈ ite x ≤ 0, 0, s(x -1)
to its list of assertions, which after rewriting becomes

∀ s x. ite x ≤ 0, s(x) ≈ 0, s(x) ≈ s(x -1)
By specifying the command-line option --fmf-fun, users can enable CVC4's finite model finding mode for recursive functions. In this mode, CVC4 will replace its list of known assertions based on the A translation before checking for satisfiability. Accordingly, the solver will output the approximation of the interpretation it used for recursive function definitions. For the example above, it outputs a model of s where only the values of s(x) for x = 0, . . . , 14 are correctly given:

0))))))))))))))) (define-fun c () Int 14))
With the --fmf-fun option enabled, CVC4 assumes that functions introduced using define-fun-rec are admissible. Admissibility must be proved externally by the usere.g., manually, using a syntactic criterion, or with the help of a termination prover. If some function definitions are not admissible, CVC4 may answer sat for an unsatisfiable problem. For example, if we add the inconsistent definition

(define-fun-rec h ((x Int)) Int (+ (h x) x))
to the above problem and run CVC4 with --fmf-fun, it wrongly answers sat.

CVC4 implements a few optimizations designed to help finding finite models of A(ϕ). Like other systems, the finite model finding capability of CVC4 incrementally fixes bounds on the cardinalities of uninterpreted types and increases these bounds until it encounters a model. When multiple types are present, it uses a fairness scheme that bounds the sum of cardinalities of all uninterpreted types [START_REF] Reynolds | Finite Model Finding in Satisfiability Modulo Theories[END_REF]. For example, if a signature has two uninterpreted types τ 1 and τ 2 , it will first search for models where |τ 1 | + |τ 2 | is at most 2, then 3, 4, and so on. To accelerate the search for models, we implemented an optimization based on statically inferring monotonic types. A monotonic type is one in which models can always be extended with additional elements of that type [START_REF] Blanchette | Monotonicity inference for higher-order formulas[END_REF][START_REF] Claessen | Sort it out with monotonicity: Translating between many-sorted and unsorted first-order logic[END_REF]. Types α f introduced by our translation A are monotonic, because ≈ is never used directly on such types [START_REF] Claessen | Sort it out with monotonicity: Translating between many-sorted and unsorted first-order logic[END_REF]. CVC4 takes advantage of this by fixing the bounds for all monotonic types simultaneously. That is, if τ 1 and τ 2 are inferred to be monotonic (regardless of whether they are present in the original problem or introduced by our translation), the solver fixes the bound for both types to be 1, then 2, and so on. This scheme allows the solver greater flexibility compared with the default scheme, and comes with no loss of generality with respect to models, since monotonic types can always be extended to have equal cardinalities. By default, CVC4 uses techniques to minimize the number of literals it considers when constructing propositional satisfying assignments for formulas [START_REF] De Moura | Relevancy propagation[END_REF]. However, we have found such techniques degrade performance for finite model finding on problems having recursive functions that are defined by cases. For this reason, we disable the techniques for problems produced from our translation.

Nunchaku

Nunchaku is a new higher-order model finder designed to be integrated with several proof assistants. The first version was released in January 2016 with support for (co)algebraic datatypes, (co)recursive functions, and (co)inductive predicates. Support for higher-order functions is in the works. We have developed an Isabelle frontend and are planning further frontends for Coq, the TLA + Proof System, and other proof assistants.

Nunchaku is a spiritual successor to Nitpick [START_REF] Blanchette | Nitpick: A counterexample generator for higher-order logic based on a relational model finder[END_REF] for Isabelle/HOL, but is developed as a standalone OCaml program, with its own input language. Whereas Nitpick generates a succession of problems where cardinalities of finite types grow at each step, Nunchaku translates its input to one first-order logic program that targets the finite model finding fragment of CVC4, including (co)algebraic datatypes [START_REF] Reynolds | A decision procedure for (co)datatypes in SMT solvers[END_REF]. Using CVC4 also allows Nunchaku to provide efficient arithmetic reasoning and to detect unsatisfiability in addition to satisfiability. We plan to integrate other tools as backends, to exploit the strengths of competing approaches.

The input syntax was inspired by that other systems based on higher-order logic (e.g., Isabelle/HOL) and by functional programming languages (e.g., OCaml). The following simple problem gives a taste of the syntax: The problem defines a datatype (nat) and two mutually recursive inductive predicates (even and odd), declares a constant m, and specifies a goal to satisfy ("m is even and nonzero"). Nunchaku quickly finds the following partial model:

data nat := 0 | Suc nat.
val m := Suc (Suc 0). val odd := fun x. if x = Suc 0 then true else ? __ . val even := fun x. if x = Suc (Suc 0) || x = 0 then true else ? __ .

The partial model gives sufficient information to the user to evaluate the goal: "2 is even if 1 is odd, 1 is odd if 0 is even, and 0 is even." Our experience with Nitpick is that users are mostly interested in the values assigned to uninterpreted constants (e.g., m).

Occasionally, the models of underspecified recursive functions are instructive. A typical example is the head function that returns the first element of a nonempty list: where the unspecified Nil case is expressed via nonterminating recursion (head xs = head xs). The tool exhibits a model in which head Nil is interpreted as a nonzero value. Internally, Nunchaku parses and types the input problem before applying a sequence of translations, each reducing the distance to the target fragment. In our example, the predicates even and odd are polarized (specialized into a pair of predicates such that one is used in positive positions and the other in negative positions), then translated into admissible recursive functions, before another pass applies the encoding described in this paper. If a model is found, it is translated back to the input language, with ? __ placeholders indicating unknown values.

data list A := Nil | Cons A (list A).
Conceptually, the sequence of transformation is a bidirectional pipeline built by composing pairs (Encode, Decode) of transformations. For each such pair, Encode translates a Σ-problem in a logic L to a Σ -problem in a logic L , and Decode translates a model in L over Σ into a model in L over Σ, in the spirit of institution theory [START_REF] Goguen | Institutions: Abstract model theory for specification and programming[END_REF]. The pipeline includes the following phases:

Type inference infers types and checks definitions; Monomorphization specializes polymorphic definitions on their type arguments and removes unused definitions;

Elimination of equations translates multiple-equation definitions of recursive functions into a single nested pattern matching; Specialization creates instances of functions with static arguments (i.e., an argument that is passed unchanged to all recursive calls); Polarization specializes predicates into a version used in positive positions and a version used in negative positions; Unrolling adds a decreasing argument to possibly ill-founded predicates; Skolemization introduces Skolem symbols for term variables; Elimination of (co)inductive predicates recasts a multiple-clause (co)inductive predicate definition into a recursive equation; Elimination of higher-order constructs eliminates λ-abstractions and substitutes arrays for higher-order functions; Elimination of recursion performs the encoding from Section 3; Elimination of pattern matching rewrites pattern-matching expressions using datatype discriminators and selectors; CVC4 invocation runs CVC4 to obtain a model.

Evaluation

In this section, we evaluate both the overall impact of the translation introduced in Section 3 and the performance of individual SMT techniques. We gathered 602 benchmarks from three sources, which we will refer to as IsaPlanner, Leon, and Nunchaku-Mut:

• The IsaPlanner set consists of the 79 benchmarks from the IsaPlanner suite [START_REF] Johansson | Case-analysis for rippling and inductive proof[END_REF] that do not contain higher-order functions. These benchmarks have been used recently as challenge problems for a variety of inductive theorem provers. They heavily involve recursive functions and are limited to a theory of algebraic datatypes with a signature that contains uninterpreted function symbols over these datatypes. • The Leon set consists of 166 benchmarks from the Leon repository,1 which were constructed from verification conditions on simple Scala programs. These benchmarks also heavily involve recursively defined functions over algebraic datatypes, but cover a wide variety of additional theories, including bit vectors, arrays, and both linear and nonlinear arithmetic. • The Nunchaku-Mut set consists of 357 benchmarks originating from Isabelle/HOL.

They involve (co)recursively defined functions over (co)algebraic datatypes and uninterpreted functions but no other theories. They were obtained by mutation of negated Isabelle theorems, as was done for evaluating Nitpick [START_REF] Blanchette | Nitpick: A counterexample generator for higher-order logic based on a relational model finder[END_REF]. Benchmarks created by mutation have a high likelihood of having small, easy-to-find models.

The IsaPlanner and Leon benchmarks are expressed in SMT-LIB 2.5 and are in definitional form with respect to a set of well-founded functions. The Leon tool was used to generate SMT-LIB files. A majority of these benchmarks are unsatisfiable. For each of the 245 benchmarks, we considered up to three randomly selected mutated forms of its goal ψ. In particular, we considered unique formulas that are obtained as a result of exchanging a subterm of ψ at one position with another of the same type at another position. In total, we considered 213 mutated forms of theorems from IsaPlanner and 427 mutated forms of theorems from Leon. We will call these sets IsaPlanner-Mut and Leon-Mut, respectively. Each of these benchmarks exists in two versions: with and without the A translation. Problems with A were produced by running CVC4's preprocessor.

Z3 CVC4h CVC4f CVC4fh CVC4fm ϕ A(ϕ) ϕ A(ϕ) ϕ A(ϕ) ϕ A(ϕ) ϕ A(ϕ)
For Nunchaku-Mut, the Isabelle Nunchaku frontend was used to generate thousands of Nunchaku problems from Isabelle/HOL theory files involving lists, trees, and other functional data structures. Nunchaku was then used to generate SMT-LIB files, again in two versions: with and without the A translation. Problems requiring higher-order logic were discarded, since Nunchaku does not yet support them, leaving 357 problems.

Among SMT solvers, we considered Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] and CVC4 [START_REF] Barrett | CVC4[END_REF]. Z3 runs heuristic methods for quantifier instantiation [START_REF] De Moura | Efficient E-matching for SMT solvers[END_REF] as well as methods for finding models for quantified formulas [START_REF] Ge | Complete instantiation for quantified formulas in satisfiability modulo theories[END_REF]. For CVC4, we considered four configurations, referred to as CVC4h, CVC4f, CVC4fh, and CVC4fm here. Configuration CVC4h runs heuristic and conflictbased techniques for quantifier instantiation [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF], but does not include techniques for finding models. The other configurations run the finite model finding procedure due to Reynolds et al. [START_REF] Reynolds | Finite model finding in SMT[END_REF][START_REF] Reynolds | Quantifier instantiation techniques for finite model finding in SMT[END_REF]. Configuration CVC4fh additionally incorporates heuristic quantifier instantiation as described in Section 2.3 of [START_REF] Reynolds | Quantifier instantiation techniques for finite model finding in SMT[END_REF], and CVC4fm incorporates the fairness scheme for monotonic types as described in Section 4.1.

The results are summarized in Figures 2 and3. Bold indicates the maximum of a row. The benchmarks and more detailed results are available online. 2 The figures are divided into benchmarks triggering unsat and sat responses and further into benchmarks before and after the translation A. The raw evaluation data reveals no cases in which a solver answered unsat on a benchmark ϕ and sat on its corresponding benchmark A(ϕ), or vice versa. This is consistent with our expectations and Theorem 8, since these benchmarks contain only well-founded function definitions.

Figure 2 shows that for untranslated benchmarks (the "ϕ" columns), the number of sat responses is very low across all configurations. This confirms the shortcomings of existing SMT techniques for finding models for benchmarks containing recursively defined functions. The translation A (the "A(ϕ)" columns) has a major impact. CVC4f finds 550 of the 1242 benchmarks to be satisfiable, including 9 benchmarks in the nonmutated Leon benchmark set. The two optimizations for finite model finding in CVC4 (configurations CVC4fh and CVC4fm) lead to a net gain of one satisfiable benchmark each with respect to CVC4f. The performance of Z3 for countermodels also improves dramatically, as it finds 134 more benchmarks to be satisfiable, including 5 that are not solved by CVC4f. We conclude that the translation A enables SMT solvers to find countermodels for conjectures involving recursively defined functions.

Interestingly, the translation A helps all configurations for unsat responses as well.

Z3 solves a total of 269 with the translation, whereas it solves only 251 without it. Surprisingly, the configuration CVC4f, which is not tailored for handling unsatisfiable benchmarks, solves 270 unsat benchmarks overall, which is more than both CVC4h and Z3. These results suggest that the translation does not degrade the performance of SMT solvers for unsatisfiable problems involving recursive functions, and instead often improve their performance. These results suggest that it would be interesting to try this translation in Sledgehammer [START_REF] Blanchette | Extending Sledgehammer with SMT solvers[END_REF] and to try Nunchaku also as a proof tool.

Related Work

We have already described the most closely related work, by Ge and de Moura [START_REF] Ge | Complete instantiation for quantified formulas in satisfiability modulo theories[END_REF] and by Reynolds et al. [START_REF] Reynolds | Finite model finding in SMT[END_REF][START_REF] Reynolds | Quantifier instantiation techniques for finite model finding in SMT[END_REF], earlier in this paper. The finite model finding support in the instantiation-based iProver [START_REF] Korovin | Non-cyclic sorts for first-order satisfiability[END_REF] is also close, given the similarities with SMT.

Some finite model finders are based on a reduction to a decidable logic, typically propositional logic. The translation is parameterized by upper or exact finite bounds on the cardinalities of the atomic types. This procedure was pioneered by McCune in the earlier versions of Mace (originally styled MACE) [START_REF] Mccune | A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems[END_REF]. Other conceptually similar finders are Paradox [START_REF] Claessen | New techniques that improve MACE-style model finding[END_REF] and FM-Darwin [START_REF] Baumgartner | Computing finite models by reduction to function-free clause logic[END_REF] for first-order logic with equality; the Alloy Analyzer and its backend Kodkod [START_REF] Torlak | Kodkod: A relational model finder[END_REF] for first-order relational logic; and Refute [START_REF] Weber | SAT-Based Finite Model Generation for Higher-Order Logic[END_REF] and Nitpick [START_REF] Blanchette | Nitpick: A counterexample generator for higher-order logic based on a relational model finder[END_REF] for higher-order logic. An alternative is to perform an exhaustive model search directly on the original problem. Given fixed cardinalities, the search space is represented as multidimensional tables. The procedure tries different values in the function and predicate tables, checking each time if the problem is satisfied. This approach was pioneered by FINDER [START_REF] Slaney | FINDER: Finite domain enumerator system description[END_REF] and SEM [START_REF] Zhang | SEM: A system for enumerating models[END_REF] and serves as the basis of the Alloy Analyzer's precursor [START_REF] Jackson | Nitpick: A checkable specification language[END_REF] and later versions of Mace [START_REF] Mccune | Prover9 and Mace4[END_REF].

Most of the above tools cannot cope with infinite types. Kuncak and Jackson [START_REF] Kuncak | Relational analysis of algebraic datatypes[END_REF] presented an idiom for encoding algebraic datatypes and recursive functions in Alloy, by approximating datatypes by finite subterm-closed substructures. The approach finds sound (fragments of) models for formulas in the existential-bounded-universal frag-ment (i.e., formulas whose prenex normal forms contain no unbounded universal quantifiers ranging over datatypes). This idiom was refined by Dunets et al. [START_REF] Dunets | Automated flaw detection in algebraic specifications[END_REF], who presented a translation scheme for primitive recursion. Their definedness guards play a similar role to the existential constraints generated by our translation A.

The higher-order model finder Nitpick [START_REF] Blanchette | Nitpick: A counterexample generator for higher-order logic based on a relational model finder[END_REF] for the Isabelle/HOL proof assistant relies on another variant of Kuncak and Jackson's approach inside a Kleene-style threevalued logic, inspired by abstract interpretation. It was also the first tool of its kind to support corecursion and coalgebraic datatypes [START_REF] Blanchette | Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions[END_REF]. The three-valued logic approach extends each approximated type with an unknown value, which is propagated by function application. This scheme works reasonably well in Nitpick, but experiments with CVC4 suggest that it is more efficient to avoid unknowns by adding existential constraints.

The Leon system [START_REF] Blanc | An overview of the Leon verification system-Verification by translation to recursive functions[END_REF] implements a procedure that can produce both proofs and counterexamples for properties of terminating functions written in a subset of Scala. Leon is based on an SMT solver. It avoids quantifiers altogether by unfolding recursive definitions up to a certain depth, which is increased on a per-need basis. Our translation A works in an analogous manner, but the SMT solver is invoked only once and quantifier instantiation is used in lieu of function unfolding. It would be worth investigating how existing approaches for function unfolding can inform approaches for dedicated quantifier instantiation techniques for function definitions, and vice versa.

Model finding is concerned with satisfying arbitrary logical constraints. Some tools are tailored for problems that correspond to total functional programs. QuickCheck [START_REF] Claessen | QuickCheck: A lightweight tool for random testing of Haskell programs[END_REF] for Haskell is an early example, based on random testing. Bounded exhaustive testing [START_REF] Runciman | SmallCheck and Lazy SmallCheck: Automatic exhaustive testing for small values[END_REF] and narrowing [START_REF] Lindblad | Property directed generation of first-order test data[END_REF] are other successful strategies. These tools are often much faster than model finders, but they typically cannot cope with unspecified or underspecified functions (e.g., the head function from Section 4.2). Another approach, which also fails in the face of underspecification, is to take the conjecture as an axiom and to attempt to derive a contradiction using an automatic theorem prover [START_REF] Baumgartner | Proving infinite satisfiability[END_REF]. If the other axioms are consistent (which can be checked syntactically in some cases), a contradiction imples the existence of countermodels. Compared with these approaches, the main advantage of our approach is that it can cope with underspecification and that it exploits the SMT solver (and its SAT solver) to enumerate candidate models efficiently.

Conclusion

We presented a translation scheme that extends the scope of finite model finding techniques in SMT, allowing one to use them to find models of quantified formulas over infinite types, such as integers and algebraic datatypes. In future work, it would be interesting to evaluate the approach against other counterexample generators, notably Leon, Nitpick, and Quickcheck, and enrich the benchmark suite with more problems exercising CVC4's support for coalgebraic datatypes [START_REF] Reynolds | A decision procedure for (co)datatypes in SMT solvers[END_REF]. We are also working on an encoding of higher-order functions in SMT-LIB, as a generalization to the current translation scheme, for Nunchaku. Further work would also include identifying additional sufficient conditions for admissibility, thereby enlarging the applicability of the translation scheme presented here.

Lemma 6 .Lemma 7 .Theorem 8 .

 678 Let ψ be a formula not containing function definitions, and let I be an E(Σ)-interpretation whose Σ-reduct is a model of T . Then I satisfies A(ψ) if and only if it satisfies L ∪ X(L), where L is a set of ground Σ-literals that T -entail ψ.Proof sketch. By definition of A and case analysis on the return values of A 0 . If ψ is a formula not containing function definitions, then A(ψ) T ψ. If ϕ is a Σ-formula in definitional form with respect to Σ dfn and the set of function definitions ∆ corresponding to Σ dfn is admissible, then ϕ and A(ϕ) are equisatisfiable in T .

  fun s (($x1 Int)) Int (ite (= $x1 14) 105 (ite (= $x1 13) 91 (ite (= $x1 12) 78 (ite (= $x1 11) 66 (ite (= $x1 10) 55 (ite (= $x1 4) 10 (ite (= $x1 9) 45 (ite (= $x1 8) 36 (ite (= $x1 7) 28 (ite (= $x1 6) 21 (ite (= $x1 3) 6 (ite (= $x1 5) 15 (ite (= $x1 2) 3 (ite (= $x1 1) 1

  pred even : nat -> prop := even 0;forall n. odd n => even (Suc n) and odd : nat -> prop := forall n. even n => odd (Suc n).val m : nat. goal even m && ~(m = 0).

  rec head : pi A. list A -> A := forall y ys. head (Cons y ys) = y. goal ~(head Nil = 0). Nunchaku transforms the definition of head into head xs = match xs with Nil -> head xs | Cons y ys -> y end

  Number of unsat responses on benchmarks without and with A translation

	IsaPlanner	0	0	0	0	0	0	0	0	0	0
	IsaPlanner-Mut	0 41	0	0	0 153	0 153	0	153
	Leon	0	2	0	0	0	9	0	9	0	10
	Leon-Mut	11 78	6	6	6 189	6 189	6	189
	Nunchaku-Mut	3 27	0	0	3 199	2 200	2	199
	Total	14 148	6	6	8 550	8 551	8	551
	Fig. 2. Number of sat responses on benchmarks without and with A translation
		Z3			CVC4h	CVC4f	CVC4fh	CVC4fm
		ϕ A(ϕ)		ϕ A(ϕ) ϕ A(ϕ)		ϕ A(ϕ) ϕ A(ϕ)
	IsaPlanner	14 15	15 15	1	15	15 15	1	15
	IsaPlanner-Mut	18 18	18 18	4	18	18 18	4	18
	Leon	74 79	80 80 17	78	80 77 17	78
	Leon-Mut	84 98	104 98 24 100	104 98 24 100
	Nunchaku-Mut	61 59	46 53 45	59	44 59 45	59
	Total	251 269 263 264 91 270 261 267 91 270
	Fig. 3.

https://github.com/epfl-lara/leon/

http://cs.uiowa.edu/~ajreynol/IJCAR2016-recfun

Acknowledgments. Viktor Kuncak and Stephan Merz have made this work possible. We would also like to thank Damien Busato-Gaston and Emmanouil Koukoutos for providing the set of Leon benchmarks used in the evaluation, and Mark Summerfield for suggesting several textual improvements. Cruanes is supported by the Inria technological development action "Contreexemples utilisables par Isabelle et Coq" (CUIC).