Assert(!done());
TNode assertion = get();
- if( options::finiteModelFind() ){
+ if( options::finiteModelFind() && d_quantEngine && d_quantEngine->getBoundedIntegers() ){
d_quantEngine->getBoundedIntegers()->assertNode(assertion);
}
d_model_engine = new quantifiers::ModelEngine( c, this );
d_modules.push_back( d_model_engine );
- d_bint = new quantifiers::BoundedIntegers( c, this );
- d_modules.push_back( d_bint );
+ //d_bint = new quantifiers::BoundedIntegers( c, this );
+ //d_modules.push_back( d_bint );
+ d_bint = NULL;
}else{
d_model_engine = NULL;
d_bint = NULL;
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision
-DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf
+DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf
BINARY = cvc4
LOG_COMPILER = @srcdir@/../run_regression
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+; EXIT: 10
+;%--------------------------------------------------------------------------
+;% File : ALG008-1 : TPTP v5.4.0. Released v2.2.0.
+;% Domain : General Algebra
+;% Problem : TC + right identity does not give RC.
+;% Version : [MP96] (equality) axioms : Especial.
+;% English : An algebra with a right identity satisfying the Thomsen
+;% Closure (RC) condition does not necessarily satisfy the
+;% Reidemeister Closure (RC) condition.
+
+;% Refs : [McC98] McCune (1998), Email to G. Sutcliffe
+;% : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq
+;% Source : [McC98]
+;% Names : TC-3 [MP96]
+
+;% Status : Satisfiable
+;% Rating : 0.50 v5.4.0, 0.80 v5.3.0, 0.78 v5.2.0, 0.80 v5.0.0, 0.78 v4.1.0, 0.71 v4.0.1, 0.80 v4.0.0, 0.50 v3.7.0, 0.33 v3.4.0, 0.50 v3.3.0, 0.33 v3.2.0, 0.80 v3.1.0, 0.67 v2.7.0, 0.33 v2.6.0, 0.86 v2.5.0, 0.50 v2.4.0, 0.67 v2.3.0, 1.00 v2.2.1
+;% Syntax : Number of clauses : 6 ( 0 non-Horn; 5 unit; 5 RR)
+;% Number of atoms : 10 ( 10 equality)
+;% Maximal clause size : 5 ( 2 average)
+;% Number of predicates : 1 ( 0 propositional; 2-2 arity)
+;% Number of functors : 9 ( 8 constant; 0-2 arity)
+;% Number of variables : 9 ( 0 singleton)
+;% Maximal term depth : 2 ( 2 average)
+;% SPC : CNF_SAT_RFO_EQU_NUE
+
+;% Comments : The smallest model has 3 elements.
+;%--------------------------------------------------------------------------
+;%----Thomsen Closure (TC) condition:
+(set-logic UF)
+(set-info :status sat)
+(declare-sort sort__smt2 0)
+; functions
+(declare-fun multiply__smt2_2 ( sort__smt2 sort__smt2 ) sort__smt2)
+(declare-fun identity__smt2_0 ( ) sort__smt2)
+(declare-fun c4__smt2_0 ( ) sort__smt2)
+(declare-fun a__smt2_0 ( ) sort__smt2)
+(declare-fun c3__smt2_0 ( ) sort__smt2)
+(declare-fun b__smt2_0 ( ) sort__smt2)
+(declare-fun c2__smt2_0 ( ) sort__smt2)
+(declare-fun c1__smt2_0 ( ) sort__smt2)
+(declare-fun f__smt2_0 ( ) sort__smt2)
+; predicates
+
+; thomsen_closure axiom
+(assert (forall ((?V7 sort__smt2) (?V6 sort__smt2) (?W sort__smt2) (?V sort__smt2) (?U sort__smt2) (?Z sort__smt2) (?Y sort__smt2) (?X sort__smt2))
+ (or (not (= (multiply__smt2_2 ?X ?Y) ?Z))
+ (not (= (multiply__smt2_2 ?U ?V) ?Z))
+ (not (= (multiply__smt2_2 ?X ?W) ?V6))
+ (not (= (multiply__smt2_2 ?V7 ?V) ?V6))
+ (= (multiply__smt2_2 ?U ?W) (multiply__smt2_2 ?V7 ?Y)))) )
+
+;%----Right identity:
+; right_identity axiom
+(assert (forall ((?X sort__smt2)) (= (multiply__smt2_2 ?X identity__smt2_0) ?X)) )
+
+;%----Denial of Reidimeister Closure (RC) condidition.
+; prove_reidimeister1 negated_conjecture
+(assert (= (multiply__smt2_2 c4__smt2_0 a__smt2_0) (multiply__smt2_2 c3__smt2_0 b__smt2_0)) )
+
+; prove_reidimeister2 negated_conjecture
+(assert (= (multiply__smt2_2 c2__smt2_0 a__smt2_0) (multiply__smt2_2 c1__smt2_0 b__smt2_0)) )
+
+; prove_reidimeister3 negated_conjecture
+(assert (= (multiply__smt2_2 c4__smt2_0 f__smt2_0) (multiply__smt2_2 c3__smt2_0 identity__smt2_0)) )
+
+; prove_reidimeister4 negated_conjecture
+(assert (not (= (multiply__smt2_2 c2__smt2_0 f__smt2_0) (multiply__smt2_2 c1__smt2_0 identity__smt2_0))) )
+
+
+(check-sat)
--- /dev/null
+% COMMAND-LINE: --finite-model-find
+% EXPECT: unsat
+% EXIT: 20
+(benchmark Isabelle
+:status sat
+:logic AUFLIA
+:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11 S12 S13 S14 S15 S16 S17 S18 S19 S20 S21 S22 S23 S24 S25 S26 S27 S28 S29 S30 S31 S32 S33 S34 S35 S36 S37)
+:extrafuns (
+ (f1 S1)
+ (f2 S1)
+ (f3 S3 S2 S1)
+ (f4 S4 S2 S3)
+ (f5 S4)
+ (f6 S6 S5 S1)
+ (f7 S7 S5 S6)
+ (f8 S7)
+ (f9 S9 S8 S1)
+ (f10 S10 S8 S9)
+ (f11 S10)
+ (f12 S1)
+ (f13 S12 S1)
+ (f14 S12)
+ (f15 S12 S1)
+ (f16 S2)
+ (f17 S13 S2 S2)
+ (f18 S14 S11 S13)
+ (f19 S14)
+ (f20 S5)
+ (f21 S16 S5 S5)
+ (f22 S17 S15 S16)
+ (f23 S17)
+ (f24 S8)
+ (f25 S18 S8 S8)
+ (f26 S19 S5 S18)
+ (f27 S19)
+ (f28 S20 S2 S13)
+ (f29 S20)
+ (f30 S21 S5 S16)
+ (f31 S21)
+ (f32 S22 S8 S18)
+ (f33 S22)
+ (f34 S14)
+ (f35 S17)
+ (f36 S19)
+ (f37 S24 S23 S2)
+ (f38 S25 S2 S24)
+ (f39 S25)
+ (f40 S26 S23 S1)
+ (f41 S27 Int S26)
+ (f42 S27)
+ (f43 S28 S23 S5)
+ (f44 S29 S5 S28)
+ (f45 S29)
+ (f46 S30 S23 S8)
+ (f47 S31 S8 S30)
+ (f48 S31)
+ (f49 S2 S1)
+ (f50 S5 S1)
+ (f51 S8 S1)
+ (f52 S4)
+ (f53 S7)
+ (f54 S10)
+ (f55 S32 S2 S11)
+ (f56 S32)
+ (f57 S33 S5 S15)
+ (f58 S33)
+ (f59 S34 S8 S5)
+ (f60 S34)
+ (f61 S35 S11 S1)
+ (f62 S2 S35)
+ (f63 S36 S15 S1)
+ (f64 S5 S36)
+ (f65 S8 S6)
+ (f66 S35 S3)
+ (f67 S36 S6)
+ (f68 S6 S9)
+ (f69 S11 S3)
+ (f70 S5 S9)
+ (f71 S15 S6)
+ (f72 S13)
+ (f73 S16)
+ (f74 S18)
+ (f75 S20)
+ (f76 S21)
+ (f77 S22)
+ (f78 S37 S26 Int)
+ (f79 S37)
+)
+:assumption (not (= f1 f2))
+:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (forall (?v0 S5) (?v1 S5) (iff (= (f6 (f7 f8 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (forall (?v0 S8) (?v1 S8) (iff (= (f9 (f10 f11 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (not (= f12 f1))
+:assumption (forall (?v0 S11) (?v1 S11) (implies (not (= ?v0 ?v1)) (= f12 f1)))
+:assumption (exists (?v0 S11) (?v1 S11) (?v2 S11) (distinct ?v0 ?v1 ?v2))
+:assumption (exists (?v0 S11) (?v1 S11) (?v2 S11) (distinct ?v0 ?v1 ?v2) )
+:assumption (= (f13 f14) f1)
+:assumption (= (f15 f14) f1)
+:assumption (forall (?v0 S11) (?v1 S11) (implies (not (= ?v0 ?v1)) (exists (?v2 S11) (distinct ?v0 ?v1 ?v2))) )
+:assumption (forall (?v0 S11) (?v1 S2) (not (= f16 (f17 (f18 f19 ?v0) ?v1))) )
+:assumption (forall (?v0 S15) (?v1 S5) (not (= f20 (f21 (f22 f23 ?v0) ?v1))) )
+:assumption (forall (?v0 S5) (?v1 S8) (not (= f24 (f25 (f26 f27 ?v0) ?v1))) )
+:assumption (forall (?v0 S11) (?v1 S2) (not (= (f17 (f18 f19 ?v0) ?v1) f16)) )
+:assumption (forall (?v0 S15) (?v1 S5) (not (= (f21 (f22 f23 ?v0) ?v1) f20)) )
+:assumption (forall (?v0 S5) (?v1 S8) (not (= (f25 (f26 f27 ?v0) ?v1) f24)) )
+:assumption (forall (?v0 S2) (iff (not (= ?v0 f16)) (exists (?v1 S11) (?v2 S2) (= ?v0 (f17 (f18 f19 ?v1) ?v2)))) )
+:assumption (forall (?v0 S5) (iff (not (= ?v0 f20)) (exists (?v1 S15) (?v2 S5) (= ?v0 (f21 (f22 f23 ?v1) ?v2)))) )
+:assumption (forall (?v0 S8) (iff (not (= ?v0 f24)) (exists (?v1 S5) (?v2 S8) (= ?v0 (f25 (f26 f27 ?v1) ?v2)))) )
+:assumption (forall (?v0 S2) (implies (implies (= ?v0 f16) false) (implies (forall (?v1 S11) (?v2 S2) (implies (= ?v0 (f17 (f18 f19 ?v1) ?v2)) false)) false)) )
+:assumption (forall (?v0 S5) (implies (implies (= ?v0 f20) false) (implies (forall (?v1 S15) (?v2 S5) (implies (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false)) false)) )
+:assumption (forall (?v0 S8) (implies (implies (= ?v0 f24) false) (implies (forall (?v1 S5) (?v2 S8) (implies (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false)) false)) )
+:assumption (forall (?v0 S2) (?v1 S11) (not (= ?v0 (f17 (f18 f19 ?v1) ?v0))) )
+:assumption (forall (?v0 S8) (?v1 S5) (not (= ?v0 (f25 (f26 f27 ?v1) ?v0))) )
+:assumption (forall (?v0 S5) (?v1 S15) (not (= ?v0 (f21 (f22 f23 ?v1) ?v0))) )
+:assumption (forall (?v0 S11) (?v1 S2) (not (= (f17 (f18 f19 ?v0) ?v1) ?v1)) )
+:assumption (forall (?v0 S5) (?v1 S8) (not (= (f25 (f26 f27 ?v0) ?v1) ?v1)) )
+:assumption (forall (?v0 S15) (?v1 S5) (not (= (f21 (f22 f23 ?v0) ?v1) ?v1)) )
+:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (?v3 S2) (iff (= (f17 (f18 f19 ?v0) ?v1) (f17 (f18 f19 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) )
+:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8) (iff (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) )
+:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (?v3 S5) (iff (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) )
+:assumption (forall (?v0 S11) (?v1 S2) (= (f17 (f28 f29 (f17 (f18 f19 ?v0) ?v1)) f16) (f17 (f18 f19 ?v0) ?v1)) )
+:assumption (forall (?v0 S15) (?v1 S5) (= (f21 (f30 f31 (f21 (f22 f23 ?v0) ?v1)) f20) (f21 (f22 f23 ?v0) ?v1)) )
+:assumption (forall (?v0 S5) (?v1 S8) (= (f25 (f32 f33 (f25 (f26 f27 ?v0) ?v1)) f24) (f25 (f26 f27 ?v0) ?v1)) )
+:assumption (forall (?v0 S11) (= (f17 (f18 f34 ?v0) f16) (f17 (f18 f19 ?v0) f16)) )
+:assumption (forall (?v0 S15) (= (f21 (f22 f35 ?v0) f20) (f21 (f22 f23 ?v0) f20)) )
+:assumption (forall (?v0 S5) (= (f25 (f26 f36 ?v0) f24) (f25 (f26 f27 ?v0) f24)) )
+:assumption (forall (?v0 S2) (?v1 S3) (implies (not (= ?v0 f16)) (implies (forall (?v2 S11) (= (f3 ?v1 (f17 (f18 f19 ?v2) f16)) f1)) (implies (forall (?v2 S11) (?v3 S2) (implies (not (= ?v3 f16)) (implies (= (f3 ?v1 ?v3) f1) (= (f3 ?v1 (f17 (f18 f19 ?v2) ?v3)) f1)))) (= (f3 ?v1 ?v0) f1)))) )
+:assumption (forall (?v0 S5) (?v1 S6) (implies (not (= ?v0 f20)) (implies (forall (?v2 S15) (= (f6 ?v1 (f21 (f22 f23 ?v2) f20)) f1)) (implies (forall (?v2 S15) (?v3 S5) (implies (not (= ?v3 f20)) (implies (= (f6 ?v1 ?v3) f1) (= (f6 ?v1 (f21 (f22 f23 ?v2) ?v3)) f1)))) (= (f6 ?v1 ?v0) f1)))) )
+:assumption (forall (?v0 S8) (?v1 S9) (implies (not (= ?v0 f24)) (implies (forall (?v2 S5) (= (f9 ?v1 (f25 (f26 f27 ?v2) f24)) f1)) (implies (forall (?v2 S5) (?v3 S8) (implies (not (= ?v3 f24)) (implies (= (f9 ?v1 ?v3) f1) (= (f9 ?v1 (f25 (f26 f27 ?v2) ?v3)) f1)))) (= (f9 ?v1 ?v0) f1)))) )
+:assumption (forall (?v0 S11) (?v1 S23) (= (f37 (f38 f39 (f17 (f18 f19 ?v0) f16)) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) (f17 (f18 f19 ?v0) f16) f16)) )
+:assumption (forall (?v0 S15) (?v1 S23) (= (f43 (f44 f45 (f21 (f22 f23 ?v0) f20)) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) (f21 (f22 f23 ?v0) f20) f20)) )
+:assumption (forall (?v0 S5) (?v1 S23) (= (f46 (f47 f48 (f25 (f26 f27 ?v0) f24)) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) (f25 (f26 f27 ?v0) f24) f24)) )
+:assumption (forall (?v0 S23) (= (f37 (f38 f39 f16) ?v0) f16) )
+:assumption (forall (?v0 S23) (= (f43 (f44 f45 f20) ?v0) f20) )
+:assumption (forall (?v0 S23) (= (f46 (f47 f48 f24) ?v0) f24) )
+:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (?v3 S2) (= (f17 (f28 f29 (f17 (f18 f19 ?v0) ?v1)) (f17 (f18 f19 ?v2) ?v3)) (f17 (f18 f19 ?v0) (f17 (f18 f19 ?v2) (f17 (f28 f29 ?v1) ?v3)))) )
+:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8) (= (f25 (f32 f33 (f25 (f26 f27 ?v0) ?v1)) (f25 (f26 f27 ?v2) ?v3)) (f25 (f26 f27 ?v0) (f25 (f26 f27 ?v2) (f25 (f32 f33 ?v1) ?v3)))) )
+:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (?v3 S5) (= (f21 (f30 f31 (f21 (f22 f23 ?v0) ?v1)) (f21 (f22 f23 ?v2) ?v3)) (f21 (f22 f23 ?v0) (f21 (f22 f23 ?v2) (f21 (f30 f31 ?v1) ?v3)))) )
+:assumption (forall (?v0 S2) (= (f17 (f28 f29 ?v0) f16) ?v0) )
+:assumption (forall (?v0 S5) (= (f21 (f30 f31 ?v0) f20) ?v0) )
+:assumption (forall (?v0 S8) (= (f25 (f32 f33 ?v0) f24) ?v0) )
+:assumption (forall (?v0 S2) (= (f17 (f28 f29 f16) ?v0) ?v0) )
+:assumption (forall (?v0 S5) (= (f21 (f30 f31 f20) ?v0) ?v0) )
+:assumption (forall (?v0 S8) (= (f25 (f32 f33 f24) ?v0) ?v0) )
+:assumption (forall (?v0 S2) (iff (= ?v0 f16) (= (f49 ?v0) f1)) )
+:assumption (forall (?v0 S5) (iff (= ?v0 f20) (= (f50 ?v0) f1)) )
+:assumption (forall (?v0 S8) (iff (= ?v0 f24) (= (f51 ?v0) f1)) )
+:assumption (forall (?v0 S2) (iff (= (f49 ?v0) f1) (= ?v0 f16)) )
+:assumption (forall (?v0 S5) (iff (= (f50 ?v0) f1) (= ?v0 f20)) )
+:assumption (forall (?v0 S8) (iff (= (f51 ?v0) f1) (= ?v0 f24)) )
+:assumption (iff (= (f49 f16) f1) true)
+:assumption (iff (= (f50 f20) f1) true)
+:assumption (iff (= (f51 f24) f1) true)
+:assumption (forall (?v0 S11) (?v1 S2) (iff (= (f49 (f17 (f18 f19 ?v0) ?v1)) f1) false) )
+:assumption (forall (?v0 S5) (?v1 S8) (iff (= (f51 (f25 (f26 f27 ?v0) ?v1)) f1) false) )
+:assumption (forall (?v0 S15) (?v1 S5) (iff (= (f50 (f21 (f22 f23 ?v0) ?v1)) f1) false) )
+:assumption (forall (?v0 S2) (iff (= (f3 (f4 f52 ?v0) f16) f1) (= (f49 ?v0) f1)) )
+:assumption (forall (?v0 S5) (iff (= (f6 (f7 f53 ?v0) f20) f1) (= (f50 ?v0) f1)) )
+:assumption (forall (?v0 S8) (iff (= (f9 (f10 f54 ?v0) f24) f1) (= (f51 ?v0) f1)) )
+:assumption (forall (?v0 S11) (?v1 S2) (= (f55 f56 (f17 (f18 f19 ?v0) ?v1)) (ite (= ?v1 f16) ?v0 (f55 f56 ?v1))) )
+:assumption (forall (?v0 S15) (?v1 S5) (= (f57 f58 (f21 (f22 f23 ?v0) ?v1)) (ite (= ?v1 f20) ?v0 (f57 f58 ?v1))) )
+:assumption (forall (?v0 S5) (?v1 S8) (= (f59 f60 (f25 (f26 f27 ?v0) ?v1)) (ite (= ?v1 f24) ?v0 (f59 f60 ?v1))) )
+:assumption (forall (?v0 S2) (?v1 S11) (implies (not (= ?v0 f16)) (= (f55 f56 (f17 (f18 f19 ?v1) ?v0)) (f55 f56 ?v0))) )
+:assumption (forall (?v0 S5) (?v1 S15) (implies (not (= ?v0 f20)) (= (f57 f58 (f21 (f22 f23 ?v1) ?v0)) (f57 f58 ?v0))) )
+:assumption (forall (?v0 S8) (?v1 S5) (implies (not (= ?v0 f24)) (= (f59 f60 (f25 (f26 f27 ?v1) ?v0)) (f59 f60 ?v0))) )
+:assumption (forall (?v0 S2) (?v1 S11) (implies (= ?v0 f16) (= (f55 f56 (f17 (f18 f19 ?v1) ?v0)) ?v1)) )
+:assumption (forall (?v0 S5) (?v1 S15) (implies (= ?v0 f20) (= (f57 f58 (f21 (f22 f23 ?v1) ?v0)) ?v1)) )
+:assumption (forall (?v0 S8) (?v1 S5) (implies (= ?v0 f24) (= (f59 f60 (f25 (f26 f27 ?v1) ?v0)) ?v1)) )
+:assumption (forall (?v0 S11) (iff (= (f61 (f62 f16) ?v0) f1) false) )
+:assumption (forall (?v0 S15) (iff (= (f63 (f64 f20) ?v0) f1) false) )
+:assumption (forall (?v0 S5) (iff (= (f6 (f65 f24) ?v0) f1) false) )
+:assumption (forall (?v0 S35) (iff (= (f3 (f66 ?v0) f16) f1) false) )
+:assumption (forall (?v0 S36) (iff (= (f6 (f67 ?v0) f20) f1) false) )
+:assumption (forall (?v0 S6) (iff (= (f9 (f68 ?v0) f24) f1) false) )
+:assumption (forall (?v0 S11) (?v1 S2) (= (f3 (f69 ?v0) (f17 (f18 f19 ?v0) ?v1)) f1) )
+:assumption (forall (?v0 S5) (?v1 S8) (= (f9 (f70 ?v0) (f25 (f26 f27 ?v0) ?v1)) f1) )
+:assumption (forall (?v0 S15) (?v1 S5) (= (f6 (f71 ?v0) (f21 (f22 f23 ?v0) ?v1)) f1) )
+:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (iff (= (f61 (f62 (f17 (f18 f19 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f61 (f62 ?v1) ?v2) f1))) )
+:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (iff (= (f6 (f65 (f25 (f26 f27 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f6 (f65 ?v1) ?v2) f1))) )
+:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (iff (= (f63 (f64 (f21 (f22 f23 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f63 (f64 ?v1) ?v2) f1))) )
+:assumption (forall (?v0 S8) (?v1 S8) (iff (= (f9 (f10 f54 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (forall (?v0 S5) (?v1 S5) (iff (= (f6 (f7 f53 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f52 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (= (f17 f72 f16) f16)
+:assumption (= (f21 f73 f20) f20)
+:assumption (= (f25 f74 f24) f24)
+:assumption (forall (?v0 S11) (?v1 S2) (= (f17 f72 (f17 (f18 f19 ?v0) ?v1)) (ite (= ?v1 f16) f16 (f17 (f18 f19 ?v0) (f17 f72 ?v1)))) )
+:assumption (forall (?v0 S15) (?v1 S5) (= (f21 f73 (f21 (f22 f23 ?v0) ?v1)) (ite (= ?v1 f20) f20 (f21 (f22 f23 ?v0) (f21 f73 ?v1)))) )
+:assumption (forall (?v0 S5) (?v1 S8) (= (f25 f74 (f25 (f26 f27 ?v0) ?v1)) (ite (= ?v1 f24) f24 (f25 (f26 f27 ?v0) (f25 f74 ?v1)))) )
+:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (implies (= (f3 (f69 ?v0) ?v1) f1) (= (f3 (f69 ?v0) (f17 (f18 f19 ?v2) ?v1)) f1)) )
+:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (implies (= (f9 (f70 ?v0) ?v1) f1) (= (f9 (f70 ?v0) (f25 (f26 f27 ?v2) ?v1)) f1)) )
+:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (implies (= (f6 (f71 ?v0) ?v1) f1) (= (f6 (f71 ?v0) (f21 (f22 f23 ?v2) ?v1)) f1)) )
+:assumption (forall (?v0 S2) (implies (not (= ?v0 f16)) (= (f17 (f28 f75 (f17 f72 ?v0)) (f17 (f18 f19 (f55 f56 ?v0)) f16)) ?v0)) )
+:assumption (forall (?v0 S5) (implies (not (= ?v0 f20)) (= (f21 (f30 f76 (f21 f73 ?v0)) (f21 (f22 f23 (f57 f58 ?v0)) f20)) ?v0)) )
+:assumption (forall (?v0 S8) (implies (not (= ?v0 f24)) (= (f25 (f32 f77 (f25 f74 ?v0)) (f25 (f26 f27 (f59 f60 ?v0)) f24)) ?v0)) )
+:assumption (forall (?v0 S2) (?v1 S11) (?v2 S2) (iff (= (f17 (f28 f75 ?v0) (f17 (f18 f19 ?v1) f16)) ?v2) (and (not (= ?v2 f16)) (and (= (f17 f72 ?v2) ?v0) (= (f55 f56 ?v2) ?v1)))) )
+:assumption (forall (?v0 S5) (?v1 S15) (?v2 S5) (iff (= (f21 (f30 f76 ?v0) (f21 (f22 f23 ?v1) f20)) ?v2) (and (not (= ?v2 f20)) (and (= (f21 f73 ?v2) ?v0) (= (f57 f58 ?v2) ?v1)))) )
+:assumption (forall (?v0 S8) (?v1 S5) (?v2 S8) (iff (= (f25 (f32 f77 ?v0) (f25 (f26 f27 ?v1) f24)) ?v2) (and (not (= ?v2 f24)) (and (= (f25 f74 ?v2) ?v0) (= (f59 f60 ?v2) ?v1)))) )
+:assumption (= f11 f54)
+:assumption (= f8 f53)
+:assumption (= f5 f52)
+:assumption (forall (?v0 S8) (?v1 S8) (iff (= (f9 (f10 f54 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (forall (?v0 S5) (?v1 S5) (iff (= (f6 (f7 f53 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f52 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (forall (?v0 S8) (iff (= (f9 (f10 f54 ?v0) ?v0) f1) true) )
+:assumption (forall (?v0 S5) (iff (= (f6 (f7 f53 ?v0) ?v0) f1) true) )
+:assumption (forall (?v0 S2) (iff (= (f3 (f4 f52 ?v0) ?v0) f1) true) )
+:assumption (= f54 f11)
+:assumption (= f53 f8)
+:assumption (= f52 f5)
+:assumption (forall (?v0 S11) (?v1 S2) (iff (= (f3 (f69 ?v0) ?v1) f1) (or (exists (?v2 S11) (?v3 S2) (and (= ?v0 ?v2) (= ?v1 (f17 (f18 f19 ?v2) ?v3)))) (exists (?v2 S11) (?v3 S2) (?v4 S11) (and (= ?v0 ?v2) (and (= ?v1 (f17 (f18 f19 ?v4) ?v3)) (= (f3 (f69 ?v2) ?v3) f1)))))) )
+:assumption (forall (?v0 S5) (?v1 S8) (iff (= (f9 (f70 ?v0) ?v1) f1) (or (exists (?v2 S5) (?v3 S8) (and (= ?v0 ?v2) (= ?v1 (f25 (f26 f27 ?v2) ?v3)))) (exists (?v2 S5) (?v3 S8) (?v4 S5) (and (= ?v0 ?v2) (and (= ?v1 (f25 (f26 f27 ?v4) ?v3)) (= (f9 (f70 ?v2) ?v3) f1)))))) )
+:assumption (forall (?v0 S15) (?v1 S5) (iff (= (f6 (f71 ?v0) ?v1) f1) (or (exists (?v2 S15) (?v3 S5) (and (= ?v0 ?v2) (= ?v1 (f21 (f22 f23 ?v2) ?v3)))) (exists (?v2 S15) (?v3 S5) (?v4 S15) (and (= ?v0 ?v2) (and (= ?v1 (f21 (f22 f23 ?v4) ?v3)) (= (f6 (f71 ?v2) ?v3) f1)))))) )
+:assumption (forall (?v0 S2) (?v1 S11) (= (f55 f56 (f17 (f28 f75 ?v0) (f17 (f18 f19 ?v1) f16))) ?v1) )
+:assumption (forall (?v0 S5) (?v1 S15) (= (f57 f58 (f21 (f30 f76 ?v0) (f21 (f22 f23 ?v1) f20))) ?v1) )
+:assumption (forall (?v0 S8) (?v1 S5) (= (f59 f60 (f25 (f32 f77 ?v0) (f25 (f26 f27 ?v1) f24))) ?v1) )
+:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8) (implies (= (f25 (f32 f77 ?v0) ?v1) ?v2) (implies (= ?v3 (f25 (f32 f77 ?v1) ?v4)) (= (f25 (f32 f77 ?v0) ?v3) (f25 (f32 f77 ?v2) ?v4)))) )
+:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5) (implies (= (f21 (f30 f76 ?v0) ?v1) ?v2) (implies (= ?v3 (f21 (f30 f76 ?v1) ?v4)) (= (f21 (f30 f76 ?v0) ?v3) (f21 (f30 f76 ?v2) ?v4)))) )
+:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2) (implies (= (f17 (f28 f75 ?v0) ?v1) ?v2) (implies (= ?v3 (f17 (f28 f75 ?v1) ?v4)) (= (f17 (f28 f75 ?v0) ?v3) (f17 (f28 f75 ?v2) ?v4)))) )
+:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (iff (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v2) ?v1)) (= ?v0 ?v2)) )
+:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (iff (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v2) ?v1)) (= ?v0 ?v2)) )
+:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (iff (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v2) ?v1)) (= ?v0 ?v2)) )
+:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (iff (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v0) ?v2)) (= ?v1 ?v2)) )
+:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (iff (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v0) ?v2)) (= ?v1 ?v2)) )
+:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (iff (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v0) ?v2)) (= ?v1 ?v2)) )
+:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (iff (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v2) ?v3)) (exists (?v4 S8) (or (and (= ?v0 (f25 (f32 f77 ?v2) ?v4)) (= (f25 (f32 f77 ?v4) ?v1) ?v3)) (and (= (f25 (f32 f77 ?v0) ?v4) ?v2) (= ?v1 (f25 (f32 f77 ?v4) ?v3)))))) )
+:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (iff (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v2) ?v3)) (exists (?v4 S5) (or (and (= ?v0 (f21 (f30 f76 ?v2) ?v4)) (= (f21 (f30 f76 ?v4) ?v1) ?v3)) (and (= (f21 (f30 f76 ?v0) ?v4) ?v2) (= ?v1 (f21 (f30 f76 ?v4) ?v3)))))) )
+:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (iff (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v2) ?v3)) (exists (?v4 S2) (or (and (= ?v0 (f17 (f28 f75 ?v2) ?v4)) (= (f17 (f28 f75 ?v4) ?v1) ?v3)) (and (= (f17 (f28 f75 ?v0) ?v4) ?v2) (= ?v1 (f17 (f28 f75 ?v4) ?v3)))))) )
+:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (= (f25 (f32 f77 (f25 (f32 f77 ?v0) ?v1)) ?v2) (f25 (f32 f77 ?v0) (f25 (f32 f77 ?v1) ?v2))) )
+:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (= (f21 (f30 f76 (f21 (f30 f76 ?v0) ?v1)) ?v2) (f21 (f30 f76 ?v0) (f21 (f30 f76 ?v1) ?v2))) )
+:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (= (f17 (f28 f75 (f17 (f28 f75 ?v0) ?v1)) ?v2) (f17 (f28 f75 ?v0) (f17 (f28 f75 ?v1) ?v2))) )
+:assumption (forall (?v0 S11) (?v1 S2) (?v2 S2) (= (f17 (f28 f75 (f17 (f18 f19 ?v0) ?v1)) ?v2) (f17 (f18 f19 ?v0) (f17 (f28 f75 ?v1) ?v2))) )
+:assumption (forall (?v0 S5) (?v1 S8) (?v2 S8) (= (f25 (f32 f77 (f25 (f26 f27 ?v0) ?v1)) ?v2) (f25 (f26 f27 ?v0) (f25 (f32 f77 ?v1) ?v2))) )
+:assumption (forall (?v0 S15) (?v1 S5) (?v2 S5) (= (f21 (f30 f76 (f21 (f22 f23 ?v0) ?v1)) ?v2) (f21 (f22 f23 ?v0) (f21 (f30 f76 ?v1) ?v2))) )
+:assumption (forall (?v0 S11) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2) (implies (= (f17 (f18 f19 ?v0) ?v1) ?v2) (implies (= ?v3 (f17 (f28 f75 ?v1) ?v4)) (= (f17 (f18 f19 ?v0) ?v3) (f17 (f28 f75 ?v2) ?v4)))) )
+:assumption (forall (?v0 S5) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8) (implies (= (f25 (f26 f27 ?v0) ?v1) ?v2) (implies (= ?v3 (f25 (f32 f77 ?v1) ?v4)) (= (f25 (f26 f27 ?v0) ?v3) (f25 (f32 f77 ?v2) ?v4)))) )
+:assumption (forall (?v0 S15) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5) (implies (= (f21 (f22 f23 ?v0) ?v1) ?v2) (implies (= ?v3 (f21 (f30 f76 ?v1) ?v4)) (= (f21 (f22 f23 ?v0) ?v3) (f21 (f30 f76 ?v2) ?v4)))) )
+:assumption (forall (?v0 S2) (= (f17 (f28 f75 f16) ?v0) ?v0) )
+:assumption (forall (?v0 S5) (= (f21 (f30 f76 f20) ?v0) ?v0) )
+:assumption (forall (?v0 S8) (= (f25 (f32 f77 f24) ?v0) ?v0) )
+:assumption (forall (?v0 S2) (?v1 S2) (iff (= f16 (f17 (f28 f75 ?v0) ?v1)) (and (= ?v0 f16) (= ?v1 f16))) )
+:assumption (forall (?v0 S5) (?v1 S5) (iff (= f20 (f21 (f30 f76 ?v0) ?v1)) (and (= ?v0 f20) (= ?v1 f20))) )
+:assumption (forall (?v0 S8) (?v1 S8) (iff (= f24 (f25 (f32 f77 ?v0) ?v1)) (and (= ?v0 f24) (= ?v1 f24))) )
+:assumption (forall (?v0 S2) (= (f17 (f28 f75 ?v0) f16) ?v0) )
+:assumption (forall (?v0 S5) (= (f21 (f30 f76 ?v0) f20) ?v0) )
+:assumption (forall (?v0 S8) (= (f25 (f32 f77 ?v0) f24) ?v0) )
+:assumption (forall (?v0 S2) (?v1 S2) (iff (= ?v0 (f17 (f28 f75 ?v0) ?v1)) (= ?v1 f16)) )
+:assumption (forall (?v0 S5) (?v1 S5) (iff (= ?v0 (f21 (f30 f76 ?v0) ?v1)) (= ?v1 f20)) )
+:assumption (forall (?v0 S8) (?v1 S8) (iff (= ?v0 (f25 (f32 f77 ?v0) ?v1)) (= ?v1 f24)) )
+:assumption (forall (?v0 S2) (?v1 S2) (iff (= ?v0 (f17 (f28 f75 ?v1) ?v0)) (= ?v1 f16)) )
+:assumption (forall (?v0 S5) (?v1 S5) (iff (= ?v0 (f21 (f30 f76 ?v1) ?v0)) (= ?v1 f20)) )
+:assumption (forall (?v0 S8) (?v1 S8) (iff (= ?v0 (f25 (f32 f77 ?v1) ?v0)) (= ?v1 f24)) )
+:assumption (forall (?v0 S26) (= (f41 f42 (f78 f79 ?v0)) ?v0))
+:assumption (forall (?v0 Int) (implies (<= 0 ?v0) (= (f78 f79 (f41 f42 ?v0)) ?v0)))
+:assumption (forall (?v0 Int) (implies (< ?v0 0) (= (f78 f79 (f41 f42 ?v0)) 0)))
+:formula true)
+; solver: z3
+; timeout: 5.0
+; random seed: 1
+; arguments:
+; DISPLAY_PROOF=true
+; PROOF_MODE=2
+; -rs:1
+; MODEL=true
+; -smt
--- /dev/null
+% COMMAND-LINE: --finite-model-find
+% EXPECT: sat
+% EXIT: 10
+(benchmark Isabelle
+:status sat
+:logic AUFLIA
+:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11)
+:extrafuns (
+ (f1 S1)
+ (f2 S1)
+ (f3 S3 S2 S1)
+ (f4 S4 S2 S3)
+ (f5 S4)
+ (f6 S5 S5 S1)
+ (f7 S5)
+ (f8 S6 S5 S5)
+ (f9 S7 S6)
+ (f10 S8 S4 S7)
+ (f11 S9 S10 S8)
+ (f12 S11 S4 S9)
+ (f13 S11)
+ (f14 S4)
+ (f15 S10)
+ (f16 S4)
+ (f17 S10 S4)
+ (f18 S5 S5 S1)
+)
+:assumption (not (= f1 f2))
+:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) )
+:assumption (not (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1))
+:assumption (= (f6 f7 (f8 (f9 (f10 (f11 (f12 f13 f5) f15) (f17 f15))) f7)) f1)
+:assumption (= (f18 f7 (f8 (f9 (f10 (f11 (f12 f13 f14) f15) f16)) f7)) f1)
+:assumption (forall (?v0 S5) (= (f6 ?v0 f7) f1) )
+:assumption (forall (?v0 S4) (?v1 S10) (?v2 S4) (?v3 S4) (?v4 S10) (?v5 S4) (iff (= (f10 (f11 (f12 f13 ?v0) ?v1) ?v2) (f10 (f11 (f12 f13 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) )
+:assumption (forall (?v0 S5) (?v1 S5) (implies (= (f6 ?v0 ?v1) f1) (= (f18 ?v0 ?v1) f1)) )
+:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (implies (= (f6 ?v0 ?v1) f1) (implies (= (f6 ?v2 ?v0) f1) (= (f6 ?v2 ?v1) f1))) )
+:assumption (forall (?v0 S5) (?v1 S7) (?v2 S5) (implies (= (f6 ?v0 (f8 (f9 ?v1) f7)) f1) (implies (= (f6 ?v0 ?v2) f1) (= (f6 ?v0 (f8 (f9 ?v1) ?v2)) f1))) )
+:assumption (forall (?v0 S5) (?v1 S7) (?v2 S5) (implies (= (f6 ?v0 (f8 (f9 ?v1) ?v2)) f1) (and (= (f6 ?v0 (f8 (f9 ?v1) f7)) f1) (= (f6 ?v0 ?v2) f1))) )
+:assumption (forall (?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4) (implies (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v3)) f7)) f1) (implies (forall (?v5 S2) (?v6 S2) (implies (= (f3 (f4 ?v3 ?v5) ?v6) f1) (= (f3 (f4 ?v4 ?v5) ?v6) f1))) (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v4)) f7)) f1))) )
+:assumption (forall (?v0 S5) (?v1 S4) (?v2 S10) (?v3 S4) (?v4 S4) (implies (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v1) ?v2) ?v3)) f7)) f1) (implies (forall (?v5 S2) (?v6 S2) (implies (= (f3 (f4 ?v4 ?v5) ?v6) f1) (= (f3 (f4 ?v1 ?v5) ?v6) f1))) (= (f6 ?v0 (f8 (f9 (f10 (f11 (f12 f13 ?v4) ?v2) ?v3)) f7)) f1))) )
+:formula true)
+; solver: z3
+; timeout: 5.0
+; random seed: 1
+; arguments:
+; DISPLAY_PROOF=true
+; PROOF_MODE=2
+; -rs:1
+; MODEL=true
+; -smt
--- /dev/null
+BINARY = cvc4
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+ $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \
+ $(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS = \
+ agree466.smt2 \
+ ALG008-1.smt2 \
+ german169.smt2 \
+ Hoare-z3.931718.smt \
+ QEpres-uf.855035.smt \
+ agree467.smt2 \
+ Arrow_Order-smtlib.778341.smt \
+ german73.smt2 \
+ PUZ001+1.smt2 \
+ refcount24.cvc.smt2
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+# error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+# error.cvc
+
+# synonyms for "check" in this directory
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unsat
+; EXIT: 20
+;%------------------------------------------------------------------------------
+;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0.
+;% Domain : Puzzles
+;% Problem : Dreadbury Mansion
+;% Version : Especial.
+;% Theorem formulation : Reduced > Complete.
+;% English : Someone who lives in Dreadbury Mansion killed Aunt Agatha.
+;% Agatha, the butler, and Charles live in Dreadbury Mansion,
+;% and are the only people who live therein. A killer always
+;% hates his victim, and is never richer than his victim.
+;% Charles hates no one that Aunt Agatha hates. Agatha hates
+;% everyone except the butler. The butler hates everyone not
+;% richer than Aunt Agatha. The butler hates everyone Aunt
+;% Agatha hates. No one hates everyone. Agatha is not the
+;% butler. Therefore : Agatha killed herself.
+
+;% Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au
+;% : [Hah94] Haehnle (1994), Email to G. Sutcliffe
+;% Source : [Hah94]
+;% Names : Pelletier 55 [Pel86]
+
+;% Status : Theorem
+;% Rating : 0.07 v5.3.0, 0.19 v5.2.0, 0.00 v5.0.0, 0.08 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0, 0.17 v2.7.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.00 v2.1.0
+;% Syntax : Number of formulae : 14 ( 6 unit)
+;% Number of atoms : 24 ( 5 equality)
+;% Maximal formula depth : 5 ( 3 average)
+;% Number of connectives : 16 ( 6 ~; 2 |; 1 &)
+;% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
+;% ( 0 ~|; 0 ~&)
+;% Number of predicates : 5 ( 0 propositional; 1-2 arity)
+;% Number of functors : 3 ( 3 constant; 0-0 arity)
+;% Number of variables : 12 ( 0 sgn; 10 !; 2 ?)
+;% Maximal term depth : 1 ( 1 average)
+;% SPC : FOF_THM_RFO_SEQ
+
+;% Comments : Modified by Geoff Sutcliffe.
+;% : Also known as "Who killed Aunt Agatha"
+;%------------------------------------------------------------------------------
+;%----Problem axioms
+(set-logic UF)
+(set-info :status unsat)
+(declare-sort sort__smt2 0)
+; functions
+(declare-fun agatha__smt2_0 ( ) sort__smt2)
+(declare-fun butler__smt2_0 ( ) sort__smt2)
+(declare-fun charles__smt2_0 ( ) sort__smt2)
+; predicates
+(declare-fun lives__smt2_1 ( sort__smt2 ) Bool)
+(declare-fun killed__smt2_2 ( sort__smt2 sort__smt2 ) Bool)
+(declare-fun hates__smt2_2 ( sort__smt2 sort__smt2 ) Bool)
+(declare-fun richer__smt2_2 ( sort__smt2 sort__smt2 ) Bool)
+
+; pel55_1 axiom
+(assert (exists ((?X sort__smt2))
+ (and (lives__smt2_1 ?X)
+ (killed__smt2_2 ?X agatha__smt2_0))))
+
+; pel55_2_1 axiom
+(assert (lives__smt2_1 agatha__smt2_0))
+
+; pel55_2_2 axiom
+(assert (lives__smt2_1 butler__smt2_0))
+
+; pel55_2_3 axiom
+(assert (lives__smt2_1 charles__smt2_0))
+
+; pel55_3 axiom
+(assert (forall ((?X sort__smt2))
+ (=> (lives__smt2_1 ?X)
+ (or (= ?X agatha__smt2_0)
+ (= ?X butler__smt2_0)
+ (= ?X charles__smt2_0)))))
+
+; pel55_4 axiom
+(assert (forall ((?X sort__smt2) (?Y sort__smt2))
+ (=> (killed__smt2_2 ?X ?Y)
+ (hates__smt2_2 ?X ?Y))))
+
+; pel55_5 axiom
+(assert (forall ((?X sort__smt2) (?Y sort__smt2))
+ (=> (killed__smt2_2 ?X ?Y)
+ (not (richer__smt2_2 ?X ?Y)))))
+
+; pel55_6 axiom
+(assert (forall ((?X sort__smt2))
+ (=> (hates__smt2_2 agatha__smt2_0 ?X)
+ (not (hates__smt2_2 charles__smt2_0 ?X)))))
+
+; pel55_7 axiom
+(assert (forall ((?X sort__smt2))
+ (=> (not (= ?X butler__smt2_0))
+ (hates__smt2_2 agatha__smt2_0 ?X))))
+
+; pel55_8 axiom
+(assert (forall ((?X sort__smt2))
+ (=> (not (richer__smt2_2 ?X agatha__smt2_0))
+ (hates__smt2_2 butler__smt2_0 ?X))))
+
+; pel55_9 axiom
+(assert (forall ((?X sort__smt2))
+ (=> (hates__smt2_2 agatha__smt2_0 ?X)
+ (hates__smt2_2 butler__smt2_0 ?X))))
+
+; pel55_10 axiom
+(assert (forall ((?X sort__smt2))
+(exists ((?Y sort__smt2)) (not (hates__smt2_2 ?X ?Y)))))
+
+; pel55_11 axiom
+(assert (not (= agatha__smt2_0 butler__smt2_0)))
+
+;----This is the conjecture with negated conjecture
+; pel55 conjecture
+(assert (not (killed__smt2_2 agatha__smt2_0 agatha__smt2_0)))
+
+
+(check-sat)
--- /dev/null
+% COMMAND-LINE: --finite-model-find
+% EXPECT: sat
+% EXIT: 10
+(benchmark Isabelle
+:status sat
+:logic AUFLIA
+:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11 S12 S13 S14 S15 S16 S17 S18)
+:extrafuns (
+ (f1 S1)
+ (f2 S1)
+ (f3 S2 S3 S4)
+ (f4 S2)
+ (f5 S3)
+ (f6 S4)
+ (f7 S3 S5 S1)
+ (f8 S6 S5)
+ (f9 S6)
+ (f10 S7 S6 S6)
+ (f11 S7)
+ (f12 S8 S4 S4)
+ (f13 S8)
+ (f14 S10 S3 S3)
+ (f15 S11 S9 S10)
+ (f16 S12 S4 S11)
+ (f17 S12)
+ (f18 S4 S13 S1)
+ (f19 S13)
+ (f20 S4 S1)
+ (f21 S2)
+ (f22 S10)
+ (f23 S3 S9 S1)
+ (f24 S14 S9 S9)
+ (f25 S15 S4 S14)
+ (f26 S15)
+ (f27 S13)
+ (f28 S8)
+ (f29 S16 S9 S3)
+ (f30 S17 S4 S16)
+ (f31 S18 S4 S17)
+ (f32 S18)
+ (f33 S18)
+ (f34 S4 S4 S1)
+)
+:assumption (not (= f1 f2))
+:assumption (not (not (= (f3 f4 f5) f6)))
+:assumption (forall (?v0 S3) (implies (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f4 ?v0) f6))) )
+:assumption (= (f7 f5 (f8 (f10 f11 f9))) f1)
+:assumption (forall (?v0 S4) (iff (= f6 ?v0) (= ?v0 f6)) )
+:assumption (= (f12 f13 f6) f6)
+:assumption (forall (?v0 S4) (iff (= f6 (f12 f13 ?v0)) (= ?v0 f6)) )
+:assumption (forall (?v0 S4) (iff (= (f12 f13 ?v0) f6) (= ?v0 f6)) )
+:assumption (forall (?v0 S4) (?v1 S9) (?v2 S3) (= (f3 f4 (f14 (f15 (f16 f17 ?v0) ?v1) ?v2)) (f3 f4 ?v2)) )
+:assumption (= (f18 f6 f19) f1)
+:assumption (= (f20 f6) f1)
+:assumption (forall (?v0 S4) (iff (= (f20 ?v0) f1) (= ?v0 f6)) )
+:assumption (forall (?v0 S3) (implies (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f21 ?v0) f6))) )
+:assumption (forall (?v0 S3) (implies (not (not (= (f3 f21 ?v0) f6))) (implies (not (= (f3 f4 ?v0) f6)) (not (= (f3 f4 (f14 f22 ?v0)) f6)))) )
+:assumption (forall (?v0 S4) (?v1 S4) (iff (= (f12 f13 ?v0) (f12 f13 ?v1)) (= ?v0 ?v1)) )
+:assumption (forall (?v0 S6) (?v1 S9) (implies (forall (?v2 S3) (implies (= (f7 ?v2 (f8 ?v0)) f1) (not (= (f3 f21 ?v2) f6)))) (iff (exists (?v2 S4) (forall (?v3 S3) (implies (= (f7 ?v3 (f8 (f10 f11 ?v0))) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)))) (exists (?v2 S4) (forall (?v3 S3) (implies (= (f7 ?v3 (f8 ?v0)) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)))))) )
+:assumption (forall (?v0 S4) (= (f18 (f12 f13 ?v0) f27) f1) )
+:assumption (= (f12 f28 f6) f6)
+:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (= (f3 f4 (f29 (f30 (f31 f32 ?v0) ?v1) ?v2)) ?v0) )
+:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (= (f3 f4 (f29 (f30 (f31 f33 ?v0) ?v1) ?v2)) ?v0) )
+:assumption (= (f18 f6 f27) f1)
+:assumption (forall (?v0 S3) (?v1 S4) (?v2 S9) (implies (not (not (= (f3 f21 ?v0) f6))) (iff (= (f23 ?v0 (f24 (f25 f26 ?v1) ?v2)) f1) (= (f23 (f14 f22 ?v0) ?v2) f1))) )
+:assumption (forall (?v0 S4) (iff (= (f34 (f12 f13 ?v0) f6) f1) (= (f34 ?v0 f6) f1)) )
+:assumption (forall (?v0 S4) (iff (= (f34 f6 (f12 f13 ?v0)) f1) (= (f34 f6 ?v0) f1)) )
+:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (not (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5))) )
+:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (not (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5))) )
+:assumption (forall (?v0 S4) (= (f34 ?v0 ?v0) f1) )
+:assumption (forall (?v0 S4) (?v1 S4) (or (= (f34 ?v0 ?v1) f1) (= (f34 ?v1 ?v0) f1)) )
+:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (iff (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) )
+:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (iff (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) )
+:assumption (forall (?v0 S4) (?v1 S4) (?v2 S4) (implies (= (f34 ?v0 ?v1) f1) (implies (= (f34 ?v1 ?v2) f1) (= (f34 ?v0 ?v2) f1))) )
+:assumption (forall (?v0 S4) (?v1 S4) (implies (= (f34 ?v0 ?v1) f1) (implies (= (f34 ?v1 ?v0) f1) (= ?v0 ?v1))) )
+:formula true)
+; solver: z3
+; timeout: 1.897
+; random seed: 1
+; arguments:
+; DISPLAY_PROOF=true
+; PROOF_MODE=2
+; -rs:1
+; MODEL=true
+; -smt
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+; EXIT: 10
+; Preamble --------------
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ((UNIT (Unit))))
+(declare-datatypes () ((BOOL (Truth) (Falsity))))
+
+; Decls --------------
+(declare-sort node$type 0)
+(declare-sort value$type 0)
+(define-sort Nodes$elem$type () node$type)
+(declare-sort Nodes$t$type 0)
+(declare-fun Nodes$empty () Nodes$t$type)
+(declare-fun Nodes$mem (Nodes$elem$type Nodes$t$type) BOOL)
+(declare-fun Nodes$add (Nodes$elem$type Nodes$t$type) Nodes$t$type)
+(declare-fun Nodes$remove (Nodes$elem$type Nodes$t$type) Nodes$t$type)
+(declare-fun Nodes$cardinality (Nodes$t$type) Int)
+(declare-fun Nodes$union (Nodes$t$type Nodes$t$type) Nodes$t$type)
+(declare-fun Nodes$disjoint (Nodes$t$type Nodes$t$type) BOOL)
+;Nodes$disjoint_empty :
+(assert (forall ((a Nodes$t$type)) (= (Nodes$disjoint a Nodes$empty) Truth)))
+;Nodes$disjoint_comm :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$disjoint a b)
+ (Nodes$disjoint b a))))
+;Nodes$mem_empty :
+(assert (forall ((e Nodes$elem$type)) (not (= (Nodes$mem e Nodes$empty)
+ Truth))))
+;Nodes$mem_add :
+(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type))
+ (= (Nodes$mem x (Nodes$add y s)) (ite (or (= x y) (= (Nodes$mem x s)
+ Truth)) Truth
+ Falsity))))
+;Nodes$mem_remove :
+(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type))
+ (= (Nodes$mem x (Nodes$remove y s)) (ite (and (not (= x y)) (=
+ (Nodes$mem
+ x s)
+ Truth))
+ Truth Falsity))))
+;Nodes$mem_union1 :
+(assert (forall ((x Nodes$elem$type) (a Nodes$t$type)) (=> (= (Nodes$mem x a)
+ Truth) (forall
+ ((b Nodes$t$type))
+ (=
+ (Nodes$mem
+ x (Nodes$union
+ a b))
+ Truth)))))
+;Nodes$mem_union2 :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$union a b)
+ (Nodes$union b a))))
+;Nodes$mem_union3 :
+(assert (forall ((x Nodes$elem$type) (a Nodes$t$type) (b Nodes$t$type))
+ (=> (= (Nodes$mem x (Nodes$union a b)) Truth) (or (= (Nodes$mem x a)
+ Truth) (= (Nodes$mem
+ x b)
+ Truth)))))
+;Nodes$mem_union4 :
+(assert (forall ((a Nodes$t$type)) (= (Nodes$union a a) a)))
+;Nodes$mem_union5 :
+(assert (forall ((a Nodes$t$type)) (= (Nodes$union a Nodes$empty) a)))
+;Nodes$empty_union :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$union a b)
+ Nodes$empty)
+ (= a Nodes$empty))))
+;Nodes$card_empty :
+(assert (= (Nodes$cardinality Nodes$empty) 0))
+;Nodes$card_zero :
+(assert (forall ((s Nodes$t$type)) (=> (= (Nodes$cardinality s) 0) (=
+ s
+ Nodes$empty))))
+;Nodes$card_non_negative :
+(assert (forall ((s Nodes$t$type)) (>= (Nodes$cardinality s) 0)))
+;Nodes$card_add :
+(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality
+ (Nodes$add x s))
+ (ite (= (Nodes$mem
+ x s) Truth)
+ (Nodes$cardinality
+ s) (+ (Nodes$cardinality
+ s) 1)))))
+;Nodes$card_remove :
+(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality
+ (Nodes$remove x s))
+ (ite (= (Nodes$mem
+ x s) Truth) (-
+ (Nodes$cardinality
+ s) 1) (Nodes$cardinality
+ s)))))
+;Nodes$card_union :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$disjoint
+ a b) Truth)
+ (= (Nodes$cardinality
+ (Nodes$union a b)) (+
+ (Nodes$cardinality
+ a) (Nodes$cardinality b))))))
+(declare-fun Nodes$eq (Nodes$t$type Nodes$t$type) BOOL)
+;Nodes$eq_is_equality :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$eq a b)
+ (ite (= a b) Truth
+ Falsity))))
+;Nodes$equal1 :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (forall ((x Nodes$elem$type))
+ (= (Nodes$mem x a)
+ (Nodes$mem x b)))
+ (= (Nodes$eq a b)
+ Truth))))
+(define-sort Values$elem$type () value$type)
+(declare-sort Values$t$type 0)
+(declare-fun Values$empty () Values$t$type)
+(declare-fun Values$mem (Values$elem$type Values$t$type) BOOL)
+(declare-fun Values$add (Values$elem$type Values$t$type) Values$t$type)
+(declare-fun Values$remove (Values$elem$type Values$t$type) Values$t$type)
+(declare-fun Values$cardinality (Values$t$type) Int)
+(declare-fun Values$union (Values$t$type Values$t$type) Values$t$type)
+(declare-fun Values$disjoint (Values$t$type Values$t$type) BOOL)
+;Values$disjoint_empty :
+(assert (forall ((a Values$t$type)) (= (Values$disjoint a Values$empty)
+ Truth)))
+;Values$disjoint_comm :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$disjoint
+ a b) (Values$disjoint
+ b a))))
+;Values$mem_empty :
+(assert (forall ((e Values$elem$type)) (not (= (Values$mem e Values$empty)
+ Truth))))
+;Values$mem_add :
+(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type))
+ (= (Values$mem x (Values$add y s)) (ite (or (= x y) (= (Values$mem
+ x s) Truth))
+ Truth Falsity))))
+;Values$mem_remove :
+(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type))
+ (= (Values$mem x (Values$remove y s)) (ite (and (not (= x y))
+ (= (Values$mem x s)
+ Truth)) Truth Falsity))))
+;Values$mem_union1 :
+(assert (forall ((x Values$elem$type) (a Values$t$type)) (=> (= (Values$mem
+ x a)
+ Truth) (forall
+ (
+ (b Values$t$type))
+ (=
+ (Values$mem
+ x
+ (Values$union
+ a b))
+ Truth)))))
+;Values$mem_union2 :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$union a b)
+ (Values$union b a))))
+;Values$mem_union3 :
+(assert (forall ((x Values$elem$type) (a Values$t$type) (b Values$t$type))
+ (=> (= (Values$mem x (Values$union a b)) Truth) (or (= (Values$mem
+ x a) Truth)
+ (= (Values$mem x b)
+ Truth)))))
+;Values$mem_union4 :
+(assert (forall ((a Values$t$type)) (= (Values$union a a) a)))
+;Values$mem_union5 :
+(assert (forall ((a Values$t$type)) (= (Values$union a Values$empty) a)))
+;Values$empty_union :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$union
+ a b) Values$empty)
+ (= a Values$empty))))
+;Values$card_empty :
+(assert (= (Values$cardinality Values$empty) 0))
+;Values$card_zero :
+(assert (forall ((s Values$t$type)) (=> (= (Values$cardinality s) 0)
+ (= s Values$empty))))
+;Values$card_non_negative :
+(assert (forall ((s Values$t$type)) (>= (Values$cardinality s) 0)))
+;Values$card_add :
+(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality
+ (Values$add x s))
+ (ite (= (Values$mem
+ x s)
+ Truth)
+ (Values$cardinality
+ s) (+ (Values$cardinality
+ s) 1)))))
+;Values$card_remove :
+(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality
+ (Values$remove
+ x s)) (ite
+ (=
+ (Values$mem
+ x s)
+ Truth) (-
+ (Values$cardinality
+ s)
+ 1)
+ (Values$cardinality
+ s)))))
+;Values$card_union :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$disjoint
+ a b) Truth)
+ (= (Values$cardinality
+ (Values$union a b)) (+
+ (Values$cardinality
+ a) (Values$cardinality
+ b))))))
+(declare-fun Values$eq (Values$t$type Values$t$type) BOOL)
+;Values$eq_is_equality :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$eq a b)
+ (ite (= a b) Truth
+ Falsity))))
+;Values$equal1 :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (forall ((x Values$elem$type))
+ (= (Values$mem x a)
+ (Values$mem
+ x b))) (= (Values$eq
+ a b)
+ Truth))))
+(define-sort node_set$type () (Array node$type BOOL))
+(declare-fun mk_array_1 () (Array node$type BOOL))
+;mk_array_1_def :
+(assert (forall ((mk_array_1_index node$type)) (= (select mk_array_1
+ mk_array_1_index) Falsity)))
+(define-fun empty_node_set () node_set$type mk_array_1)
+(define-sort node_pair_set$type () (Array node$type (Array node$type BOOL)))
+(declare-fun mk_array_2 () (Array node$type BOOL))
+;mk_array_2_def :
+(assert (forall ((mk_array_2_index node$type)) (= (select mk_array_2
+ mk_array_2_index) Falsity)))
+(declare-fun mk_array_3 () (Array node$type (Array node$type BOOL)))
+;mk_array_3_def :
+(assert (forall ((mk_array_3_index node$type)) (= (select mk_array_3
+ mk_array_3_index) mk_array_2)))
+(define-fun empty_node_pair_set () node_pair_set$type mk_array_3)
+(declare-fun mk_array_4 () (Array node$type BOOL))
+;mk_array_4_def :
+(assert (forall ((mk_array_4_index node$type)) (= (select mk_array_4
+ mk_array_4_index) Truth)))
+(declare-fun mk_array_5 () (Array node$type (Array node$type BOOL)))
+;mk_array_5_def :
+(assert (forall ((mk_array_5_index node$type)) (= (select mk_array_5
+ mk_array_5_index) mk_array_4)))
+(define-fun full_node_pair_set () node_pair_set$type mk_array_5)
+(declare-fun input () (Array node$type value$type))
+(declare-fun t () Int)
+;positive_bound :
+(assert (> t 0))
+(define-sort message$type () Values$t$type)
+(define-sort message_set$type () (Array node$type message$type))
+(define-sort state$type () Values$t$type)
+(define-sort state_set$type () (Array node$type state$type))
+(define-fun null_message () message$type Values$empty)
+(declare-fun mk_array_6 () (Array node$type message$type))
+;mk_array_6_def :
+(assert (forall ((mk_array_6_index node$type)) (= (select mk_array_6
+ mk_array_6_index) null_message)))
+(define-fun null_message_set () message_set$type mk_array_6)
+(define-fun null_state () state$type Values$empty)
+(declare-fun mk_array_7 () (Array node$type state$type))
+;mk_array_7_def :
+(assert (forall ((mk_array_7_index node$type)) (= (select mk_array_7
+ mk_array_7_index) null_state)))
+(define-fun null_state_set () state_set$type mk_array_7)
+(declare-fun choose (Values$t$type) value$type)
+;choosen_value :
+(assert (forall ((vals Values$t$type)) (or (= vals Values$empty) (= (Values$mem
+ (choose
+ vals)
+ vals)
+ Truth))))
+(define-sort failure_pattern$type () node_pair_set$type)
+(define-fun is_faulty ((p node$type) (deliver failure_pattern$type)) BOOL
+(ite (exists ((q node$type)) (not (= (select (select deliver p) q) Truth)))
+Truth Falsity))
+(define-fun is_silent ((p node$type) (deliver failure_pattern$type)) BOOL
+(ite (forall ((q node$type)) (not (= (select (select deliver p) q) Truth)))
+Truth Falsity))
+(declare-datatypes () ((phase_state$type (init_phase) (send_phase) (recv_phase) (comp_phase))))
+(declare-datatypes () ((clean_state$type (before) (active) (after))))
+
+; Var Decls --------------
+(declare-fun my_compute$result$1 () state$type)
+(declare-fun output$1 () (Array node$type value$type))
+(declare-fun comp_done () node_set$type)
+(declare-fun compute$can_decide$0$1 () BOOL)
+(declare-fun chosen () (Array node$type BOOL))
+(declare-fun recv_done () node_pair_set$type)
+(declare-fun output () (Array node$type value$type))
+(declare-fun phase () phase_state$type)
+(declare-fun global_state () state_set$type)
+(declare-fun my_decide$result$1 () value$type)
+(declare-fun round () Int)
+(declare-fun compute$n () node$type)
+(declare-fun send_done () node_pair_set$type)
+(declare-fun my_can_decide$result$1 () BOOL)
+(declare-fun chosen$1 () (Array node$type BOOL))
+(declare-fun comp_done$1 () node_set$type)
+(declare-fun global_state$1 () state_set$type)
+
+; Asserts --------------
+(assert (not (=> (forall ((n node$type)) (=>
+ (and
+ (=
+ (select
+ chosen
+ n)
+ Truth)
+ (=
+ round (+
+ t
+ 1)))
+ (and
+ (forall
+ (
+ (n node$type) (m node$type))
+ (=
+ (select
+ (select
+ send_done
+ n)
+ m)
+ Truth))
+ (forall
+ (
+ (n node$type) (m node$type))
+ (=
+ (select
+ (select
+ recv_done
+ n)
+ m)
+ Truth)))))
+ (=> (= phase comp_phase) (=>
+ (not
+ (= (select
+ comp_done
+ compute$n)
+ Truth))
+ (=>
+ (= my_compute$result$1
+ (select
+ global_state
+ compute$n))
+ (=>
+ (= global_state$1
+ (store
+ global_state
+ compute$n
+ my_compute$result$1))
+ (=>
+ (= my_can_decide$result$1
+ (ite
+ (= round (+
+ t 1))
+ Truth
+ Falsity))
+ (=>
+ (= compute$can_decide$0$1
+ my_can_decide$result$1)
+ (= (ite
+ (=
+ compute$can_decide$0$1
+ Truth)
+ (ite
+ (=>
+ (=
+ my_decide$result$1
+ (choose
+ (select
+ global_state$1
+ compute$n)))
+ (=>
+ (=
+ output$1
+ (store
+ output
+ compute$n
+ my_decide$result$1))
+ (=>
+ (=
+ chosen$1
+ (store
+ chosen
+ compute$n
+ Truth))
+ (=>
+ (=
+ comp_done$1
+ (store
+ comp_done
+ compute$n
+ Truth))
+ (forall
+ (
+ (n node$type))
+ (=>
+ (and
+ (=
+ (select
+ chosen$1
+ n)
+ Truth)
+ (=
+ round (+
+ t
+ 1)))
+ (and
+ (forall
+ (
+ (n node$type) (m node$type))
+ (=
+ (select
+ (select
+ send_done
+ n)
+ m)
+ Truth))
+ (forall
+ (
+ (n node$type) (m node$type))
+ (=
+ (select
+ (select
+ recv_done
+ n)
+ m)
+ Truth)))))))))
+ Truth
+ Falsity)
+ (ite
+ (=>
+ (=
+ comp_done$1
+ (store
+ comp_done
+ compute$n
+ Truth))
+ (forall
+ (
+ (n node$type))
+ (=>
+ (and
+ (=
+ (select
+ chosen
+ n)
+ Truth)
+ (=
+ round (+
+ t
+ 1)))
+ (and
+ (forall
+ (
+ (n node$type) (m node$type))
+ (=
+ (select
+ (select
+ send_done
+ n)
+ m)
+ Truth))
+ (forall
+ (
+ (n node$type) (m node$type))
+ (=
+ (select
+ (select
+ recv_done
+ n)
+ m)
+ Truth))))))
+ Truth
+ Falsity))
+ Truth))))))))))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unsat
+; EXIT: 20
+; Preamble --------------
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((UNIT (Unit))))
+(declare-datatypes () ((BOOL (Truth) (Falsity))))
+
+; Decls --------------
+(declare-sort node$type 0)
+(declare-sort value$type 0)
+(define-sort Nodes$elem$type () node$type)
+(declare-sort Nodes$t$type 0)
+(declare-fun Nodes$empty () Nodes$t$type)
+(declare-fun Nodes$mem (Nodes$elem$type Nodes$t$type) BOOL)
+(declare-fun Nodes$add (Nodes$elem$type Nodes$t$type) Nodes$t$type)
+(declare-fun Nodes$remove (Nodes$elem$type Nodes$t$type) Nodes$t$type)
+(declare-fun Nodes$cardinality (Nodes$t$type) Int)
+(declare-fun Nodes$union (Nodes$t$type Nodes$t$type) Nodes$t$type)
+(declare-fun Nodes$disjoint (Nodes$t$type Nodes$t$type) BOOL)
+;Nodes$disjoint_empty :
+(assert (forall ((a Nodes$t$type)) (= (Nodes$disjoint a Nodes$empty) Truth)))
+;Nodes$disjoint_comm :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$disjoint a b)
+ (Nodes$disjoint b a))))
+;Nodes$mem_empty :
+(assert (forall ((e Nodes$elem$type)) (not (= (Nodes$mem e Nodes$empty)
+ Truth))))
+;Nodes$mem_add :
+(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type))
+ (= (Nodes$mem x (Nodes$add y s)) (ite (or (= x y) (= (Nodes$mem x s)
+ Truth)) Truth
+ Falsity))))
+;Nodes$mem_remove :
+(assert (forall ((x Nodes$elem$type) (y Nodes$elem$type) (s Nodes$t$type))
+ (= (Nodes$mem x (Nodes$remove y s)) (ite (and (not (= x y)) (=
+ (Nodes$mem
+ x s)
+ Truth))
+ Truth Falsity))))
+;Nodes$mem_union1 :
+(assert (forall ((x Nodes$elem$type) (a Nodes$t$type)) (=> (= (Nodes$mem x a)
+ Truth) (forall
+ ((b Nodes$t$type))
+ (=
+ (Nodes$mem
+ x (Nodes$union
+ a b))
+ Truth)))))
+;Nodes$mem_union2 :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$union a b)
+ (Nodes$union b a))))
+;Nodes$mem_union3 :
+(assert (forall ((x Nodes$elem$type) (a Nodes$t$type) (b Nodes$t$type))
+ (=> (= (Nodes$mem x (Nodes$union a b)) Truth) (or (= (Nodes$mem x a)
+ Truth) (= (Nodes$mem
+ x b)
+ Truth)))))
+;Nodes$mem_union4 :
+(assert (forall ((a Nodes$t$type)) (= (Nodes$union a a) a)))
+;Nodes$mem_union5 :
+(assert (forall ((a Nodes$t$type)) (= (Nodes$union a Nodes$empty) a)))
+;Nodes$empty_union :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$union a b)
+ Nodes$empty)
+ (= a Nodes$empty))))
+;Nodes$card_empty :
+(assert (= (Nodes$cardinality Nodes$empty) 0))
+;Nodes$card_zero :
+(assert (forall ((s Nodes$t$type)) (=> (= (Nodes$cardinality s) 0) (=
+ s
+ Nodes$empty))))
+;Nodes$card_non_negative :
+(assert (forall ((s Nodes$t$type)) (>= (Nodes$cardinality s) 0)))
+;Nodes$card_add :
+(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality
+ (Nodes$add x s))
+ (ite (= (Nodes$mem
+ x s) Truth)
+ (Nodes$cardinality
+ s) (+ (Nodes$cardinality
+ s) 1)))))
+;Nodes$card_remove :
+(assert (forall ((x Nodes$elem$type) (s Nodes$t$type)) (= (Nodes$cardinality
+ (Nodes$remove x s))
+ (ite (= (Nodes$mem
+ x s) Truth) (-
+ (Nodes$cardinality
+ s) 1) (Nodes$cardinality
+ s)))))
+;Nodes$card_union :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (= (Nodes$disjoint
+ a b) Truth)
+ (= (Nodes$cardinality
+ (Nodes$union a b)) (+
+ (Nodes$cardinality
+ a) (Nodes$cardinality b))))))
+(declare-fun Nodes$eq (Nodes$t$type Nodes$t$type) BOOL)
+;Nodes$eq_is_equality :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (= (Nodes$eq a b)
+ (ite (= a b) Truth
+ Falsity))))
+;Nodes$equal1 :
+(assert (forall ((a Nodes$t$type) (b Nodes$t$type)) (=> (forall ((x Nodes$elem$type))
+ (= (Nodes$mem x a)
+ (Nodes$mem x b)))
+ (= (Nodes$eq a b)
+ Truth))))
+(define-sort Values$elem$type () value$type)
+(declare-sort Values$t$type 0)
+(declare-fun Values$empty () Values$t$type)
+(declare-fun Values$mem (Values$elem$type Values$t$type) BOOL)
+(declare-fun Values$add (Values$elem$type Values$t$type) Values$t$type)
+(declare-fun Values$remove (Values$elem$type Values$t$type) Values$t$type)
+(declare-fun Values$cardinality (Values$t$type) Int)
+(declare-fun Values$union (Values$t$type Values$t$type) Values$t$type)
+(declare-fun Values$disjoint (Values$t$type Values$t$type) BOOL)
+;Values$disjoint_empty :
+(assert (forall ((a Values$t$type)) (= (Values$disjoint a Values$empty)
+ Truth)))
+;Values$disjoint_comm :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$disjoint
+ a b) (Values$disjoint
+ b a))))
+;Values$mem_empty :
+(assert (forall ((e Values$elem$type)) (not (= (Values$mem e Values$empty)
+ Truth))))
+;Values$mem_add :
+(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type))
+ (= (Values$mem x (Values$add y s)) (ite (or (= x y) (= (Values$mem
+ x s) Truth))
+ Truth Falsity))))
+;Values$mem_remove :
+(assert (forall ((x Values$elem$type) (y Values$elem$type) (s Values$t$type))
+ (= (Values$mem x (Values$remove y s)) (ite (and (not (= x y))
+ (= (Values$mem x s)
+ Truth)) Truth Falsity))))
+;Values$mem_union1 :
+(assert (forall ((x Values$elem$type) (a Values$t$type)) (=> (= (Values$mem
+ x a)
+ Truth) (forall
+ (
+ (b Values$t$type))
+ (=
+ (Values$mem
+ x
+ (Values$union
+ a b))
+ Truth)))))
+;Values$mem_union2 :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$union a b)
+ (Values$union b a))))
+;Values$mem_union3 :
+(assert (forall ((x Values$elem$type) (a Values$t$type) (b Values$t$type))
+ (=> (= (Values$mem x (Values$union a b)) Truth) (or (= (Values$mem
+ x a) Truth)
+ (= (Values$mem x b)
+ Truth)))))
+;Values$mem_union4 :
+(assert (forall ((a Values$t$type)) (= (Values$union a a) a)))
+;Values$mem_union5 :
+(assert (forall ((a Values$t$type)) (= (Values$union a Values$empty) a)))
+;Values$empty_union :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$union
+ a b) Values$empty)
+ (= a Values$empty))))
+;Values$card_empty :
+(assert (= (Values$cardinality Values$empty) 0))
+;Values$card_zero :
+(assert (forall ((s Values$t$type)) (=> (= (Values$cardinality s) 0)
+ (= s Values$empty))))
+;Values$card_non_negative :
+(assert (forall ((s Values$t$type)) (>= (Values$cardinality s) 0)))
+;Values$card_add :
+(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality
+ (Values$add x s))
+ (ite (= (Values$mem
+ x s)
+ Truth)
+ (Values$cardinality
+ s) (+ (Values$cardinality
+ s) 1)))))
+;Values$card_remove :
+(assert (forall ((x Values$elem$type) (s Values$t$type)) (= (Values$cardinality
+ (Values$remove
+ x s)) (ite
+ (=
+ (Values$mem
+ x s)
+ Truth) (-
+ (Values$cardinality
+ s)
+ 1)
+ (Values$cardinality
+ s)))))
+;Values$card_union :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (= (Values$disjoint
+ a b) Truth)
+ (= (Values$cardinality
+ (Values$union a b)) (+
+ (Values$cardinality
+ a) (Values$cardinality
+ b))))))
+(declare-fun Values$eq (Values$t$type Values$t$type) BOOL)
+;Values$eq_is_equality :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (= (Values$eq a b)
+ (ite (= a b) Truth
+ Falsity))))
+;Values$equal1 :
+(assert (forall ((a Values$t$type) (b Values$t$type)) (=> (forall ((x Values$elem$type))
+ (= (Values$mem x a)
+ (Values$mem
+ x b))) (= (Values$eq
+ a b)
+ Truth))))
+(define-sort node_set$type () (Array node$type BOOL))
+(declare-fun mk_array_1 () (Array node$type BOOL))
+;mk_array_1_def :
+(assert (forall ((mk_array_1_index node$type)) (= (select mk_array_1
+ mk_array_1_index) Falsity)))
+(define-fun empty_node_set () node_set$type mk_array_1)
+(define-sort node_pair_set$type () (Array node$type (Array node$type BOOL)))
+(declare-fun mk_array_2 () (Array node$type BOOL))
+;mk_array_2_def :
+(assert (forall ((mk_array_2_index node$type)) (= (select mk_array_2
+ mk_array_2_index) Falsity)))
+(declare-fun mk_array_3 () (Array node$type (Array node$type BOOL)))
+;mk_array_3_def :
+(assert (forall ((mk_array_3_index node$type)) (= (select mk_array_3
+ mk_array_3_index) mk_array_2)))
+(define-fun empty_node_pair_set () node_pair_set$type mk_array_3)
+(declare-fun mk_array_4 () (Array node$type BOOL))
+;mk_array_4_def :
+(assert (forall ((mk_array_4_index node$type)) (= (select mk_array_4
+ mk_array_4_index) Truth)))
+(declare-fun mk_array_5 () (Array node$type (Array node$type BOOL)))
+;mk_array_5_def :
+(assert (forall ((mk_array_5_index node$type)) (= (select mk_array_5
+ mk_array_5_index) mk_array_4)))
+(define-fun full_node_pair_set () node_pair_set$type mk_array_5)
+(declare-fun input () (Array node$type value$type))
+(declare-fun t () Int)
+;positive_bound :
+(assert (> t 0))
+(define-sort message$type () Values$t$type)
+(define-sort message_set$type () (Array node$type message$type))
+(define-sort state$type () Values$t$type)
+(define-sort state_set$type () (Array node$type state$type))
+(define-fun null_message () message$type Values$empty)
+(declare-fun mk_array_6 () (Array node$type message$type))
+;mk_array_6_def :
+(assert (forall ((mk_array_6_index node$type)) (= (select mk_array_6
+ mk_array_6_index) null_message)))
+(define-fun null_message_set () message_set$type mk_array_6)
+(define-fun null_state () state$type Values$empty)
+(declare-fun mk_array_7 () (Array node$type state$type))
+;mk_array_7_def :
+(assert (forall ((mk_array_7_index node$type)) (= (select mk_array_7
+ mk_array_7_index) null_state)))
+(define-fun null_state_set () state_set$type mk_array_7)
+(declare-fun choose (Values$t$type) value$type)
+;choosen_value :
+(assert (forall ((vals Values$t$type)) (or (= vals Values$empty) (= (Values$mem
+ (choose
+ vals)
+ vals)
+ Truth))))
+(define-sort failure_pattern$type () node_pair_set$type)
+(define-fun is_faulty ((p node$type) (deliver failure_pattern$type)) BOOL
+(ite (exists ((q node$type)) (not (= (select (select deliver p) q) Truth)))
+Truth Falsity))
+(define-fun is_silent ((p node$type) (deliver failure_pattern$type)) BOOL
+(ite (forall ((q node$type)) (not (= (select (select deliver p) q) Truth)))
+Truth Falsity))
+(declare-datatypes () ((phase_state$type (init_phase) (send_phase) (recv_phase) (comp_phase))))
+(declare-datatypes () ((clean_state$type (before) (active) (after))))
+
+; Var Decls --------------
+(declare-fun init_done () node_set$type)
+(declare-fun crashed () Nodes$t$type)
+(declare-fun comp_done () node_set$type)
+(declare-fun chosen () (Array node$type BOOL))
+(declare-fun recv_done () node_pair_set$type)
+(declare-fun phase () phase_state$type)
+(declare-fun clean () clean_state$type)
+(declare-fun global_state () state_set$type)
+(declare-fun messages () (Array node$type message_set$type))
+(declare-fun deliver_message () failure_pattern$type)
+(declare-fun crashing () Nodes$t$type)
+(declare-fun round () Int)
+(declare-fun send_done () node_pair_set$type)
+
+; Asserts --------------
+(declare-fun mk_array_8 () (Array node$type BOOL))
+;mk_array_8_def :
+(assert (forall ((mk_array_8_index node$type)) (= (select mk_array_8
+ mk_array_8_index) Falsity)))
+(declare-fun mk_array_9 () (Array node$type message_set$type))
+;mk_array_9_def :
+(assert (forall ((mk_array_9_index node$type)) (= (select mk_array_9
+ mk_array_9_index) null_message_set)))
+(assert (not (=> (and (and (and (and (and (and (and (and (and (and (and
+ (and
+ (=
+ clean
+ before)
+ (=
+ global_state
+ null_state_set))
+ (=
+ messages
+ mk_array_9))
+ (= deliver_message
+ full_node_pair_set))
+ (= comp_done
+ empty_node_set))
+ (= recv_done empty_node_pair_set))
+ (= send_done empty_node_pair_set))
+ (= init_done empty_node_set))
+ (= phase init_phase)) (= crashing
+ Nodes$empty))
+ (= crashed Nodes$empty)) (= round 0)) (= chosen
+ mk_array_8))
+ (forall ((n node$type)) (=> (and (= (select chosen n) Truth)
+ (= round (+ t 1))) (and (forall
+ ((n node$type) (m node$type))
+ (= (select
+ (select
+ send_done
+ n)
+ m)
+ Truth))
+ (forall (
+ (n node$type) (m node$type))
+ (= (select
+ (select
+ recv_done
+ n) m)
+ Truth))))))))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+; EXIT: 10
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ((UNIT (Unit))))
+(declare-datatypes () ((BOOL (Truth) (Falsity))))
+
+; Decls --------------
+(declare-sort node$type 0)
+(declare-sort data$type 0)
+(declare-datatypes () ((cache_state$type (invalid) (shared) (exclusive))))
+(declare-datatypes () ((cache$type (c_cache$type (c_state cache_state$type) (c_data data$type)))))
+(declare-datatypes () ((msg_cmd$type (empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte))))
+(declare-datatypes () ((msg$type (c_msg$type (m_cmd msg_cmd$type) (m_data data$type)))))
+(declare-fun dummy () data$type)
+
+; Var Decls --------------
+(declare-fun memdata$1 () data$type)
+(declare-fun shrset$1 () (Array node$type BOOL))
+(declare-fun recv_invack$i () node$type)
+(declare-fun exgntd () BOOL)
+(declare-fun chan3$1 () (Array node$type msg$type))
+(declare-fun shrset () (Array node$type BOOL))
+(declare-fun exgntd$1 () BOOL)
+(declare-fun chan2 () (Array node$type msg$type))
+(declare-fun chan3 () (Array node$type msg$type))
+(declare-fun auxnode () node$type)
+(declare-fun curcmd () msg_cmd$type)
+
+; Asserts --------------
+(assert (not (=> (and (and (forall ((n node$type))
+ (=> (= (m_cmd (select
+ chan2
+ n))
+ gnte) (= exgntd
+ Truth)))
+ (forall ((n node$type))
+ (=> (= exgntd Truth)
+ (= (select shrset n)
+ (ite (= n auxnode) Truth
+ Falsity))))) (forall
+ ((n node$type))
+ (=> (=
+ (m_cmd
+ (select
+ chan3
+ n))
+ invack)
+ (= (m_cmd
+ (select
+ chan2
+ n))
+ empty))))
+ (=> (= (m_cmd (select chan3 recv_invack$i))
+ invack) (=> (not (= curcmd empty))
+ (=> (= chan3$1 (store
+ chan3
+ recv_invack$i
+ (let (
+ (vup_228
+ (select
+ chan3
+ recv_invack$i)))
+ (c_msg$type
+ empty
+ (m_data
+ vup_228)))))
+ (=> (= shrset$1 (store
+ shrset
+ recv_invack$i
+ Falsity))
+ (= (ite (= exgntd Truth)
+ (ite (=> (= exgntd$1
+ Falsity)
+ (=> (= memdata$1
+ (m_data
+ (select
+ chan3$1
+ recv_invack$i)))
+ (forall (
+ (n node$type))
+ (=> (= (m_cmd
+ (select
+ chan2
+ n))
+ gnte)
+ (= exgntd$1
+ Truth)))))
+ Truth Falsity)
+ (ite (forall (
+ (n node$type))
+ (=> (= (m_cmd
+ (select
+ chan2
+ n))
+ gnte)
+ (= exgntd
+ Truth)))
+ Truth Falsity))
+ Truth))))))))
+
+(check-sat)
+(exit)
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unsat
+; EXIT: 20
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((UNIT (Unit))))
+(declare-datatypes () ((BOOL (Truth) (Falsity))))
+
+; Decls --------------
+(declare-sort node$type 0)
+(declare-sort data$type 0)
+(declare-datatypes () ((cache_state$type (invalid) (shared) (exclusive))))
+(declare-datatypes () ((cache$type (c_cache$type (c_state cache_state$type) (c_data data$type)))))
+(declare-datatypes () ((msg_cmd$type (empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte))))
+(declare-datatypes () ((msg$type (c_msg$type (m_cmd msg_cmd$type) (m_data data$type)))))
+(declare-fun dummy () data$type)
+
+; Var Decls --------------
+(declare-fun memdata$1 () data$type)
+(declare-fun shrset$1 () (Array node$type BOOL))
+(declare-fun recv_invack$i () node$type)
+(declare-fun exgntd () BOOL)
+(declare-fun invset () (Array node$type BOOL))
+(declare-fun chan3$1 () (Array node$type msg$type))
+(declare-fun shrset () (Array node$type BOOL))
+(declare-fun exgntd$1 () BOOL)
+(declare-fun chan2 () (Array node$type msg$type))
+(declare-fun chan3 () (Array node$type msg$type))
+(declare-fun curcmd () msg_cmd$type)
+
+; Asserts --------------
+(assert (not (=> (and (forall ((n node$type))
+ (=> (= (select invset n)
+ Truth) (= (select
+ shrset
+ n) Truth)))
+ (forall ((n node$type)) (=>
+ (or
+ (=
+ (m_cmd
+ (select
+ chan2
+ n))
+ inv)
+ (=
+ (m_cmd
+ (select
+ chan3
+ n))
+ invack))
+ (not
+ (=
+ (select
+ invset
+ n)
+ Truth)))))
+ (=> (= (m_cmd (select chan3 recv_invack$i))
+ invack) (=> (not (= curcmd empty))
+ (=> (= chan3$1 (store
+ chan3
+ recv_invack$i
+ (let (
+ (vup_101
+ (select
+ chan3
+ recv_invack$i)))
+ (c_msg$type
+ empty
+ (m_data
+ vup_101)))))
+ (=> (= shrset$1 (store
+ shrset
+ recv_invack$i
+ Falsity))
+ (= (ite (= exgntd Truth)
+ (ite (=> (= exgntd$1
+ Falsity)
+ (=> (= memdata$1
+ (m_data
+ (select
+ chan3$1
+ recv_invack$i)))
+ (forall (
+ (n node$type))
+ (=> (= (select
+ invset
+ n)
+ Truth)
+ (= (select
+ shrset$1
+ n) Truth)))))
+ Truth Falsity)
+ (ite (forall (
+ (n node$type))
+ (=> (= (select
+ invset
+ n)
+ Truth)
+ (= (select
+ shrset$1
+ n) Truth)))
+ Truth Falsity))
+ Truth))))))))
+
+(check-sat)
+(exit)
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+; EXIT: 10
+(set-logic ALL_SUPPORTED)
+(set-info :smt-lib-version 2.0)
+(set-info :category "unknown")
+(set-info :status sat)
+(declare-datatypes ()
+((UNIT (Unit))
+))
+(declare-datatypes ()
+((BOOL (Truth) (Falsity))
+))
+(declare-sort resource$type 0)
+(declare-sort process$type 0)
+(declare-fun null () resource$type)
+(declare-sort S$t$type 0)
+(declare-fun S$empty () S$t$type)
+(declare-fun S$mem (process$type S$t$type) BOOL)
+(declare-fun S$add (process$type S$t$type) S$t$type)
+(declare-fun S$remove (process$type S$t$type) S$t$type)
+(declare-fun S$cardinality (S$t$type) Int)
+(assert (forall ((e process$type)) (not (= (S$mem e S$empty) Truth))))
+(assert (forall ((x process$type) (y process$type) (s S$t$type)) (= (S$mem x (S$add y s)) (ite (or (= x y) (= (S$mem x s) Truth)) Truth Falsity))))
+(assert (forall ((x process$type) (y process$type) (s S$t$type)) (= (S$mem x (S$remove y s)) (ite (and (not (= x y)) (= (S$mem x s) Truth)) Truth Falsity))))
+(assert (= (S$cardinality S$empty) 0))
+(assert (forall ((s S$t$type)) (=> (= (S$cardinality s) 0) (= s S$empty))))
+(assert (forall ((s S$t$type)) (>= (S$cardinality s) 0)))
+(assert (forall ((x process$type) (s S$t$type)) (let ((?v_0 (S$cardinality s))) (= (S$cardinality (S$add x s)) (ite (= (S$mem x s) Truth) ?v_0 (+ ?v_0 1))))))
+(assert (forall ((x process$type) (s S$t$type)) (let ((?v_0 (S$cardinality s))) (= (S$cardinality (S$remove x s)) (ite (= (S$mem x s) Truth) (- ?v_0 1) ?v_0)))))
+(declare-fun count () (Array resource$type Int))
+(declare-fun ref () (Array process$type resource$type))
+(declare-fun valid () (Array resource$type BOOL))
+(declare-fun destroy$r () resource$type)
+(declare-fun valid$1 () (Array resource$type BOOL))
+(assert (not (=> (forall ((p process$type)) (let ((?v_0 (select ref p))) (=> (not (= ?v_0 null)) (= (select valid ?v_0) Truth)))) (=> (not (= destroy$r null)) (=> (= (select valid destroy$r) Truth) (=> (= (select count destroy$r) 0) (=> (= valid$1 (store valid destroy$r Falsity)) (forall ((p process$type)) (let ((?v_1 (select ref p))) (=> (not (= ?v_1 null)) (= (select valid$1 ?v_1) Truth)))))))))))
+(check-sat)
+(exit)
projects / cvc5.git / commitdiff