Skip to content

Commit 581f84f

Browse files
ajreynolajreynol
committed
Minor fix
1 parent 662e1a9 commit 581f84f

File tree

8 files changed

+11
-7
lines changed

8 files changed

+11
-7
lines changed

‎build-debug/out/trim-d-cpc.eo‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -710,7 +710,7 @@
710710
(program $eovc_symm ((F Bool))
711711
:signature (Bool) Bool
712712
(
713-
(($eovc_symm F) (eo::define ((_v0 ($eo_proven ($eo_prog_symm ($eo_pf F))))) ($eo_requires_eq ($eo_model_is_input _v0) true ($eo_requires_eq ($eo_typeof F) Bool ($eo_requires_eq ($eo_model_sat F) true ($eo_requires_eq ($eo_model_unsat _v0) true true))))))
713+
(($eovc_symm F) (eo::define ((_v0 ($eo_proven ($eo_prog_symm ($eo_pf F))))) ($eo_requires_eq ($eo_model_is_input _v0) true ($eo_requires_eq ($eo_typeof F) Bool ($eo_requires_eq ($eo_model_sat F) true ($eo_requires_eq ($eo_typeof _v0) Bool ($eo_requires_eq ($eo_model_unsat _v0) true true)))))))
714714
)
715715
)
716716
(echo "smt-meta $eovc_symm :deps $smtx_hash $eo_reverse_hash $smtx_value_hash $smtx_reverse_value_hash $eo_smt_type $tsm_Bool $eo_Type $eo_fun_type $eo_apply $eo_mk_apply ")

‎build-debug/out/vc-def-cpc.eo‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,7 @@
169169
(program $eovc_symm ((F Bool))
170170
:signature (Bool) Bool
171171
(
172-
(($eovc_symm F) (eo::define ((_v0 ($eo_proven ($eo_prog_symm ($eo_pf F))))) ($eo_requires_eq ($eo_model_is_input _v0) true ($eo_requires_eq ($eo_typeof F) Bool ($eo_requires_eq ($eo_model_sat F) true ($eo_requires_eq ($eo_model_unsat _v0) true true))))))
172+
(($eovc_symm F) (eo::define ((_v0 ($eo_proven ($eo_prog_symm ($eo_pf F))))) ($eo_requires_eq ($eo_model_is_input _v0) true ($eo_requires_eq ($eo_typeof F) Bool ($eo_requires_eq ($eo_model_sat F) true ($eo_requires_eq ($eo_typeof _v0) Bool ($eo_requires_eq ($eo_model_unsat _v0) true true)))))))
173173
)
174174
)
175175
(echo "smt-meta $eovc_symm :deps $smtx_hash $eo_reverse_hash $smtx_value_hash $smtx_reverse_value_hash $eo_smt_type $tsm_Bool $eo_Type $eo_fun_type $eo_apply $eo_mk_apply ")

‎build-debug/out/vc/final-cpc-symm.smt2‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -528,7 +528,7 @@
528528
(ite (= x1 eo.Stuck)
529529
eo.Stuck
530530
(ite true
531-
($eo_requires_eq ($eo_model_is_input ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtTerm (sm.Boolean true)) ($eo_requires_eq ($eo_typeof x1) (eo.SmtType tsm.Bool) ($eo_requires_eq ($eo_model_sat x1) (eo.SmtTerm (sm.Boolean true)) ($eo_requires_eq ($eo_model_unsat ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtTerm (sm.Boolean true)) (eo.SmtTerm (sm.Boolean true))))))
531+
($eo_requires_eq ($eo_model_is_input ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtTerm (sm.Boolean true)) ($eo_requires_eq ($eo_typeof x1) (eo.SmtType tsm.Bool) ($eo_requires_eq ($eo_model_sat x1) (eo.SmtTerm (sm.Boolean true)) ($eo_requires_eq ($eo_typeof ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtType tsm.Bool) ($eo_requires_eq ($eo_model_unsat ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtTerm (sm.Boolean true)) (eo.SmtTerm (sm.Boolean true)))))))
532532
eo.Stuck)))
533533

534534

‎build-debug/out/vc/final-cpc-symm.sy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -528,7 +528,7 @@
528528
(ite (= x1 eo.Stuck)
529529
eo.Stuck
530530
(ite true
531-
($eo_requires_eq ($eo_model_is_input ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtTerm (sm.Boolean true)) ($eo_requires_eq ($eo_typeof x1) (eo.SmtType tsm.Bool) ($eo_requires_eq ($eo_model_sat x1) (eo.SmtTerm (sm.Boolean true)) ($eo_requires_eq ($eo_model_unsat ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtTerm (sm.Boolean true)) (eo.SmtTerm (sm.Boolean true))))))
531+
($eo_requires_eq ($eo_model_is_input ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtTerm (sm.Boolean true)) ($eo_requires_eq ($eo_typeof x1) (eo.SmtType tsm.Bool) ($eo_requires_eq ($eo_model_sat x1) (eo.SmtTerm (sm.Boolean true)) ($eo_requires_eq ($eo_typeof ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtType tsm.Bool) ($eo_requires_eq ($eo_model_unsat ($eo_proven ($eo_prog_symm (eo.Apply eo.$eo_pf x1)))) (eo.SmtTerm (sm.Boolean true)) (eo.SmtTerm (sm.Boolean true)))))))
532532
eo.Stuck)))
533533

534534

‎build-debug/out/vcm-def-cpc.eo‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1801,7 +1801,7 @@
18011801
(program $eovc_symm ((F Bool))
18021802
:signature (Bool) Bool
18031803
(
1804-
(($eovc_symm F) (eo::define ((_v0 ($eo_proven ($eo_prog_symm ($eo_pf F))))) ($eo_requires_eq ($eo_model_is_input _v0) true ($eo_requires_eq ($eo_typeof F) Bool ($eo_requires_eq ($eo_model_sat F) true ($eo_requires_eq ($eo_model_unsat _v0) true true))))))
1804+
(($eovc_symm F) (eo::define ((_v0 ($eo_proven ($eo_prog_symm ($eo_pf F))))) ($eo_requires_eq ($eo_model_is_input _v0) true ($eo_requires_eq ($eo_typeof F) Bool ($eo_requires_eq ($eo_model_sat F) true ($eo_requires_eq ($eo_typeof _v0) Bool ($eo_requires_eq ($eo_model_unsat _v0) true true)))))))
18051805
)
18061806
)
18071807
(echo "smt-meta $eovc_symm :deps $smtx_hash $eo_reverse_hash $smtx_value_hash $smtx_reverse_value_hash $eo_smt_type $tsm_Bool $eo_Type $eo_fun_type $eo_apply $eo_mk_apply ")

‎build-debug/out/vcmt-def-cpc.eo‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -460,7 +460,7 @@
460460
(program $eovc_symm ((F Bool))
461461
:signature (Bool) Bool
462462
(
463-
(($eovc_symm F) (eo::define ((_v0 ($eo_proven ($eo_prog_symm ($eo_pf F))))) ($eo_requires_eq ($eo_model_is_input _v0) true ($eo_requires_eq ($eo_typeof F) Bool ($eo_requires_eq ($eo_model_sat F) true ($eo_requires_eq ($eo_model_unsat _v0) true true))))))
463+
(($eovc_symm F) (eo::define ((_v0 ($eo_proven ($eo_prog_symm ($eo_pf F))))) ($eo_requires_eq ($eo_model_is_input _v0) true ($eo_requires_eq ($eo_typeof F) Bool ($eo_requires_eq ($eo_model_sat F) true ($eo_requires_eq ($eo_typeof _v0) Bool ($eo_requires_eq ($eo_model_unsat _v0) true true)))))))
464464
)
465465
)
466466
(echo "smt-meta $eovc_symm :deps $smtx_hash $eo_reverse_hash $smtx_value_hash $smtx_reverse_value_hash $eo_smt_type $tsm_Bool $eo_Type $eo_fun_type $eo_apply $eo_mk_apply ")

‎build-debug/run_gen_vc_single‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -123,7 +123,7 @@ if [[ "$USE_SYGUS" == "ON" ]]; then
123123

124124
echo "**** smt_meta: Check for counterexamples with sygus, args $BASE_ARGS"
125125
#$CVC5 $BASE_ARGS $SYGUS_OUT -q -o sygus-enumerator -o sygus-grammar -o sygus
126-
$CVC5 $BASE_ARGS --tlimit=120000 $SYGUS_OUT -q
126+
$CVC5 $BASE_ARGS --tlimit=60000 $SYGUS_OUT -q
127127
check_status
128128
else
129129
echo "**** smt_meta: Generate SMT2 from $VCMT_DEF_DESUGAR to $VC_OUT"

‎plugins/desugar/desugar.cpp‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -668,6 +668,10 @@ void Desugar::finalizeRule(const Expr& e)
668668
Expr unsound = d_true;
669669
// require that the conclusion is not satisfied
670670
unsound = mkRequiresModelSat(false, conclusion, unsound);
671+
if (StdPlugin::optionVcUseTypeof())
672+
{
673+
unsound = mkRequiresModelTypeofBool(conclusion, unsound);
674+
}
671675
// require that each premise is satisfied
672676
for (size_t i = 0, nargs = progCase.getNumChildren(); i < nargs; i++)
673677
{

0 commit comments

Comments
 (0)